Skip to content

Commit

Permalink
feat(sol-driver): add golden tests outputs
Browse files Browse the repository at this point in the history
  • Loading branch information
aripiprazole committed May 29, 2024
1 parent 9983ce6 commit 25db558
Show file tree
Hide file tree
Showing 2 changed files with 45 additions and 0 deletions.
34 changes: 34 additions & 0 deletions sol-driver/suite/church_encoding/church_encoding.expect
Original file line number Diff line number Diff line change
@@ -0,0 +1,34 @@

// Natural numbers
Nat
: U
= (n : U) -> (n -> n) -> n

Succ
: Nat -> Nat
= |prev n succ$ zero$| succ$ (prev n succ$ zero$) zero$

Zero
: Nat
= |n succ$ zero$| zero$

// Maybe definition
Maybe
: U -> U
= |t| (a : U) -> (t -> a) -> a -> a

Just
: {a : U} -> a -> Maybe a
= |value t just$ nothing$| just$ value

Nothing
: {a : U} -> Maybe a
= |t just$ nothing$| nothing$

Sorry
: {a : U} -> a
= Sorry

Maybe.unwrap : {a : U} -> Maybe a -> a
Maybe.unwrap = |maybe|
maybe (|value| value) Sorry
11 changes: 11 additions & 0 deletions sol-driver/suite/church_encoding/leibniz_equality.expect
Original file line number Diff line number Diff line change
@@ -0,0 +1,11 @@
Eq
: {a : U} -> a -> a -> U
= |a x y| (p : a -> U) -> p x -> p y

Eq.refl
: {a : U} -> {x : a} -> Eq a a
= |a px| px

Test_Eq_Int64_10_10
: Eq 10 10
= Eq.refl

0 comments on commit 25db558

Please sign in to comment.