git.iko.soy/Idris-dev
on master help sign in
Merge pull request #2828 from david-christiansen/pruviloj
da70923David Christiansen
libs/pruviloj/Pruviloj/Core.idr+2−2
compare with master
unifiedsplit
@@ -91,7 +91,7 @@ newHole hint ty =
91|||
91|||
92||| @ tm the term that has the right type for the hole
92||| @ tm the term that has the right type for the hole
93exact : (tm : Raw) -> Elab ()
93exact : (tm : Raw) -> Elab ()
94−exact tm = do apply tm []
94+exact tm = do fill tm
95 solve
95 solve
96
96
97||| Introduce as many names as possible, returning them.
97||| Introduce as many names as possible, returning them.
@@ -178,7 +178,7 @@ data Infer : Type where
178total
178total
179inferType : (tac : Elab ()) -> Elab (TT, TT)
179inferType : (tac : Elab ()) -> Elab (TT, TT)
180inferType tac =
180inferType tac =
181− case fst !(runElab `(Infer) (startInfer *> tac)) of
181+ case fst !(runElab `(Infer) (do startInfer; tac)) of
182 `(MkInfer ~ty ~tm) => return (tm, ty)
182 `(MkInfer ~ty ~tm) => return (tm, ty)
183 _ => fail [TextPart "Not infer"]
183 _ => fail [TextPart "Not infer"]
184 where
184 where
libs/pruviloj/Pruviloj/Derive/DecEq.idr+1−3
@@ -44,9 +44,7 @@ partial -- TODO make covering/total
44matchCase : List Raw -> Elab ()
44matchCase : List Raw -> Elab ()
45matchCase [] = search
45matchCase [] = search
46matchCase (tm :: tms) =
46matchCase (tm :: tms) =
47− do hs <- induction tm
47+ do (y :: n :: _) <- induction tm
48− y <- unsafeNth 0 hs
49− n <- unsafeNth 1 hs
50
48
51 focus n; compute
49 focus n; compute
52 contra <- gensym "contra"
50 contra <- gensym "contra"