git.iko.soy/Idris-dev
on master help sign in
Delete splitPair tactic
773f417Joomy Korkut
CHANGELOG.md+1−1
compare with master
unifiedsplit
@@ -13,7 +13,7 @@
13
13
14+ Added `Text.Literate`, a module for working with literate source files.
14+ Added `Text.Literate`, a module for working with literate source files.
15+ Added `Data.IORef`, for working with mutable references in `IO`.
15+ Added `Data.IORef`, for working with mutable references in `IO`.
16−+ Added `discriminate` and `splitPair` tactics to Pruviloj.
16++ Added `discriminate` and `construct` tactics to Pruviloj.
17
17
18## Tool Updates
18## Tool Updates
19+ Private functions are no longer visible in the REPL except for modules
19+ Private functions are no longer visible in the REPL except for modules
libs/pruviloj/Pruviloj/Core.idr−15
@@ -256,21 +256,6 @@ unproduct tm =
256 try (unproduct (Var n1))
256 try (unproduct (Var n1))
257 try (unproduct (Var n2))
257 try (unproduct (Var n2))
258
258
259−||| If the goal is a tuple or a dependent pair, then split it into
260−||| two goals and return the new goal names.
261−||| It fails if the goal is neither a `Pair` nor a `DPair`.
262−splitPair : Elab (TTName, TTName)
263−splitPair =
264− let bug = [TextPart "Splitting created wrong number of holes"] in
265− case !goalType of
266− `(Pair ~A ~B) => do [x, y] <- apply `(MkPair {A=~A} {B=~B}) [False, False]
267− | _ => fail bug
268− solve ; pure (x, y)
269− `(DPair ~A ~Pr) => do [x, y] <- apply `(MkDPair {a=~A} {P=~Pr}) [False, False]
270− | _ => fail bug
271− solve ; pure (x, y)
272− _ => fail [TextPart "Goal is not a pair"]
273−
274||| Try to apply the constructors of the goal data type one by one,
259||| Try to apply the constructors of the goal data type one by one,
275||| and apply the first one that works.
260||| and apply the first one that works.
276||| Similar to `constructor` in Coq.
261||| Similar to `constructor` in Coq.