dc69794 · Idris-dev · git.iko.soy

libs/prelude/Builtins.idr+1−1

compare with master

unifiedsplit

@@ -63,7 +63,7 @@ infix 5 ~=~

63||| @ x the left side

64||| @ y the right side

65(~=~) : (x : a) -> (y : b) -> Type

66−(~=~) x y = (=) _ _ x y

66+(~=~) x y = (x = y)

67

68||| Perform substitution in a term according to some equality.

69|||

src/Idris/AbsSyntaxTree.hs+1−1

@@ -1282,7 +1282,7 @@ getInferType (App _ (App _ _ ty) _) = ty

1282

1283-- Handy primitives: Unit, False, Pair, MkPair, =, mkForeign

1284

1285−primNames = [eqTy, eqCon, inferTy, inferCon]

1285+primNames = [inferTy, inferCon]

1286

1287unitTy = sUN "Unit"

1288unitCon = sUN "MkUnit"

test/quasiquote004/Quasiquote004.idr+1−1

@@ -5,7 +5,7 @@ import Language.Reflection

5%default total

6

7normPlus : 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

9normPlus ctxt `(S ~n) = normPlus ctxt n

10normPlus ctxt `(plus ~n (S ~m)) = Seq (Rewrite `(plusSuccRightSucc ~n ~m))

11 (normPlus ctxt m)

test/reg037/reg037.idr+3−3

@@ -1,9 +1,9 @@

1

2--- Parser regression for (=) as a function name (fnName)

3

4−class Foo (t : (A : Type) -> (B : Type) -> A -> B -> Type) where

4+class Foo (t : a -> b -> Type) where

5− foo : (A : Type) -> (B : Type) -> (x : A) -> (y : B) -> t A B x y -> t A B x y

5+ foo : (x : _) -> (y : _) -> t x y -> t x y

6

7instance Foo (=) where

8− foo A B x y prf = prf

8+ foo x y prf = prf

9

test/reg047/reg047.idr+1−1

@@ -6,7 +6,7 @@ data TTSigma : (A : Type) -> (B : A -> Type) -> Type where

6data Nat = zero | succ Nat

7

8Id : (A : Type) -> A -> A -> Type

9−Id A = (=) {a0 = A} {b0 = A}

9+Id A = (=) {A = A} {B = A}

10

11IdRefl : (A : Type) -> (a : A) -> Id A a a

12IdRefl A a = Refl {a}