Names in sym
commitd4b7dbdc60ffc19b43fe95fdca20be0f499785be
authorEdwin Brady <ecb10@st-andrews.ac.uk>
dateMon 21 Mar 2016, 22:48 (11 years ago)
parent7c2bdb4
libs/prelude/Builtins.idr+1−1
@@ -93,7 +93,7 @@ replace : {a:_} -> {x:_} -> {y:_} -> {P : a -> Type} -> x = y -> P x -> P y
9393replace Refl prf = prf
9494
9595||| Symmetry of propositional equality
96−sym : {l:a} -> {r:a} -> l = r -> r = l
96+sym : {left:a} -> {right:a} -> left = right -> right = left
9797sym Refl = Refl
9898
9999||| Transitivity of propositional equality