Skip to content

Commit

Permalink
Add recursive global equality test
Browse files Browse the repository at this point in the history
  • Loading branch information
ollef committed Mar 25, 2024
1 parent a5db482 commit b788911
Showing 1 changed file with 1 addition and 1 deletion.
Original file line number Diff line number Diff line change
Expand Up @@ -12,7 +12,7 @@ data Equals forall A. (a b : A) where
Refl : Equals a a

test : forall a b (f : a -> b) as. Equals (map f as) (map2 f as)
test = Refl --loops
test = Refl -- type mismatch error expected

test2 : forall a b (f : a -> b) as. Equals (map f as) (map2 f as)
test2 @{f, as} = case as of
Expand Down

0 comments on commit b788911

Please sign in to comment.