git.iko.soy/Idris-dev
on master help sign in
x = y now tries homogeneous equality first
4d62d30Edwin Brady
libs/prelude/Builtins.idr+8
compare with master
unifiedsplit
@@ -15,6 +15,14 @@ FalseElim : _|_ -> a
15||| For 'symbol syntax. 'foo becomes Symbol_ "foo"
15||| For 'symbol syntax. 'foo becomes Symbol_ "foo"
16data Symbol_ : String -> Type where
16data Symbol_ : String -> Type where
17
17
18+-- Eq_ : a -> a -> Type
19+-- Eq_ x y = (=) _ _ x y
20+
21+infix 5 ~=~
22+
23+(~=~) : a -> b -> Type
24+(~=~) x y = (=) _ _ x y
25+
18-- ------------------------------------------------------ [ For rewrite tactic ]
26-- ------------------------------------------------------ [ For rewrite tactic ]
19||| Perform substitution in a term according to some equality.
27||| Perform substitution in a term according to some equality.
20|||
28|||
src/Idris/ElabTerm.hs+19
@@ -250,6 +250,25 @@ elab ist info emode opts fn tm
250 elab' ina (PRefl fc t)
250 elab' ina (PRefl fc t)
251 = elab' ina (PApp fc (PRef fc eqCon) [pimp (sMN 0 "A") Placeholder True,
251 = elab' ina (PApp fc (PRef fc eqCon) [pimp (sMN 0 "A") Placeholder True,
252 pimp (sMN 0 "x") t False])
252 pimp (sMN 0 "x") t False])
253+ elab' ina (PEq fc Placeholder Placeholder l r)
254+ = try (do tyn <- getNameFrom (sMN 0 "aqty")
255+ claim tyn RType
256+ movelast tyn
257+ elab' ina (PApp fc (PRef fc eqTy)
258+ [pimp (sUN "A") (PRef fc tyn) True,
259+ pimp (sUN "B") (PRef fc tyn) False,
260+ pexp l, pexp r]))
261+ (do atyn <- getNameFrom (sMN 0 "aqty")
262+ btyn <- getNameFrom (sMN 0 "bqty")
263+ claim atyn RType
264+ movelast atyn
265+ claim btyn RType
266+ movelast btyn
267+ elab' ina (PApp fc (PRef fc eqTy)
268+ [pimp (sUN "A") (PRef fc atyn) True,
269+ pimp (sUN "B") (PRef fc btyn) False,
270+ pexp l, pexp r]))
271+
253 elab' ina (PEq fc lt rt l r) = elab' ina (PApp fc (PRef fc eqTy)
272 elab' ina (PEq fc lt rt l r) = elab' ina (PApp fc (PRef fc eqTy)
254 [pimp (sUN "A") lt True,
273 [pimp (sUN "A") lt True,
255 pimp (sUN "B") rt False,
274 pimp (sUN "B") rt False,