trans doesn't need homogeneous equalities
commit601342f0327153097e0d397e97aa44e3697eeff0
authorEdwin Brady <ecb10@st-andrews.ac.uk>
dateWed 23 Apr 2014, 19:39 (13 years ago)
parente28fbb1
libs/prelude/Builtins.idr+1−1
@@ -35,7 +35,7 @@ sym : {l:a} -> {r:a} -> l = r -> r = l
3535sym refl = refl
3636
3737||| Transitivity of propositional equality
38−trans : {a:x} -> {b:x} -> {c:x} -> a = b -> b = c -> a = c
38+trans : {a:x} -> {b:y} -> {c:z} -> a = b -> b = c -> a = c
3939trans refl refl = refl
4040
4141lazy : a -> a