Merge pull request #2245 from ahmadsalim/bug/fixequalityplicity
Removed equality from primNames, as it shouldn't be handle specially when adding implicits (the only current use).
commitdc69794cf6e65797feaa2fe5459ae9504ace0892
authorDavid Christiansen <david@davidchristiansen.dk>
dateSun 10 May 2015, 22:55 (11 years ago)
parent9df946e0cae95a
libs/prelude/Builtins.idr+1−1
@@ -63,7 +63,7 @@ infix 5 ~=~
6363||| @ x the left side
6464||| @ y the right side
6565(~=~) : (x : a) -> (y : b) -> Type
66−(~=~) x y = (=) _ _ x y
66+(~=~) x y = (x = y)
6767
6868||| Perform substitution in a term according to some equality.
6969|||
src/Idris/AbsSyntaxTree.hs+1−1
@@ -1282,7 +1282,7 @@ getInferType (App _ (App _ _ ty) _) = ty
12821282
12831283-- Handy primitives: Unit, False, Pair, MkPair, =, mkForeign
12841284
1285−primNames = [eqTy, eqCon, inferTy, inferCon]
1285+primNames = [inferTy, inferCon]
12861286
12871287unitTy = sUN "Unit"
12881288unitCon = sUN "MkUnit"
test/quasiquote004/Quasiquote004.idr+1−1
@@ -5,7 +5,7 @@ import Language.Reflection
55%default total
66
77normPlus : List (TTName, Binder TT) -> TT -> Tactic
8−normPlus ctxt `((=) {Nat} {Nat} ~x ~y) = normPlus ctxt x `Seq` normPlus ctxt y
8+normPlus ctxt `((=) {A = Nat} {B = Nat} ~x ~y) = normPlus ctxt x `Seq` normPlus ctxt y
99normPlus ctxt `(S ~n) = normPlus ctxt n
1010normPlus ctxt `(plus ~n (S ~m)) = Seq (Rewrite `(plusSuccRightSucc ~n ~m))
1111 (normPlus ctxt m)
test/reg037/reg037.idr+3−3
@@ -1,9 +1,9 @@
11
22--- Parser regression for (=) as a function name (fnName)
33
4−class Foo (t : (A : Type) -> (B : Type) -> A -> B -> Type) where
5− foo : (A : Type) -> (B : Type) -> (x : A) -> (y : B) -> t A B x y -> t A B x y
4+class Foo (t : a -> b -> Type) where
5+ foo : (x : _) -> (y : _) -> t x y -> t x y
66
77instance Foo (=) where
8− foo A B x y prf = prf
8+ foo x y prf = prf
99
test/reg047/reg047.idr+1−1
@@ -6,7 +6,7 @@ data TTSigma : (A : Type) -> (B : A -> Type) -> Type where
66data Nat = zero | succ Nat
77
88Id : (A : Type) -> A -> A -> Type
9−Id A = (=) {a0 = A} {b0 = A}
9+Id A = (=) {A = A} {B = A}
1010
1111IdRefl : (A : Type) -> (a : A) -> Id A a a
1212IdRefl A a = Refl {a}