Skip to content

Commit

Permalink
wip
Browse files Browse the repository at this point in the history
  • Loading branch information
ollef committed Mar 21, 2024
1 parent ee7260b commit 33ebef6
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 33ebef6

Please sign in to comment.