git.iko.soy/Idris-dev
on master help sign in
Idris-dev/test/basic012/basic012a.idr
10 lines 301 B history raw
1Symmetric : {c : Type} -> (c -> c -> Type) -> Type
2Symmetric {c} rel = {a : c} -> {b : c} -> rel a b -> rel b a
4record Symmetry (t : Type) (rel : t -> t -> Type) where
5 constructor MkSymmetry
6 is_symmetric : Symmetric {c=t} rel
8symmetry : {ty : Type} -> Symmetry ty (=)
9symmetry = MkSymmetry sym