d66da21 · Idris-dev · git.iko.soy

libs/prelude/Decidable/Equality.idr+1

compare with master

unifiedsplit

@@ -1,6 +1,7 @@

1module Decidable.Equality

2

3import Builtins

4+import Prelude.Basics

4import Prelude.Either

5import Prelude.Either

5import Prelude.List

6import Prelude.List

6import Prelude.Vect

7import Prelude.Vect

src/Idris/CaseSplit.hs+1

@@ -326,6 +326,7 @@ getClause l fn fp = do ty <- getInternalApp fp l

326 getNameFrom i used (PPi _ _ _ _)

327 = uniqueNameFrom (mkSupply [UN "f", UN "g"]) used

328 getNameFrom i used (PApp fc f as) = getNameFrom i used f

329+ getNameFrom i used (PEq _ _ _) = uniqueNameFrom [UN "prf"] used

329 getNameFrom i used (PRef fc f)

330 getNameFrom i used (PRef fc f)

330 = case getNameHints i f of

331 = case getNameHints i f of

331 [] -> uniqueName (UN "x") used

332 [] -> uniqueName (UN "x") used

src/Idris/ElabDecls.hs+1

@@ -511,6 +511,7 @@ elabPrims = do mapM_ (elabDecl EAll toplevel)

511 (zip

512 [inferOpts, unitOpts, falseOpts, pairOpts, eqOpts]

513 [inferDecl, unitDecl, falseDecl, pairDecl, eqDecl]))

514+ addNameHint eqTy (UN "prf")

514 elabDecl EAll toplevel elimDecl

515 elabDecl EAll toplevel elimDecl

515 mapM_ elabPrim primitives

516 mapM_ elabPrim primitives

516 -- Special case prim__believe_me because it doesn't work on just constants

517 -- Special case prim__believe_me because it doesn't work on just constants

src/Idris/REPL.hs+1

@@ -741,6 +741,7 @@ process h fn (DoProofSearch updatefile l n hints)

741 updateMeta brack [] n new = ""

742

743 addBracket False new = new

744+ addBracket True new@('(':xs) | last xs == ')' = new

744 addBracket True new | any isSpace new = '(' : new ++ ")"

745 addBracket True new | any isSpace new = '(' : new ++ ")"

745 | otherwise = new

746 | otherwise = new

746

747