Skip to content

Commit

Permalink
Feat: add etabeta test
Browse files Browse the repository at this point in the history
  • Loading branch information
AlecsFerra committed Oct 1, 2024
1 parent a9a4ab8 commit 822827e
Showing 1 changed file with 24 additions and 0 deletions.
24 changes: 24 additions & 0 deletions tests/pos/eta_cons.fq
Original file line number Diff line number Diff line change
@@ -0,0 +1,24 @@
fixpoint "--rewrite"
fixpoint "--allowho"
fixpoint "--etabeta"

constant f : (func(0 , [int; int; int]))
define f (x : int, y: int) : int = {(x + y)}

constant g : (func(0 , [int; int; int]))
define g (a : int, b: int) : int = {(b + a)}


data Ty 0 = [
| Cons {mkCons : func(0 , [int; int; int])}
]

constant Cons : (func(0 , [func(0 , [int; int; int]); Ty]))

expand [1 : True; 2 : True]

constraint:
env []
lhs {VV1 : Tuple | true }
rhs {VV2 : Tuple | (Cons f = Cons g) }
id 2 tag []

0 comments on commit 822827e

Please sign in to comment.