@@ -227,10 +227,7 @@ refine tm =
227227
228228||| A helper to extract the type representation for term.
229229getTTType : Raw -> Elab TT
230−getTTType r = do
231− env <- getEnv
232− rty <- check env r
233− pure $ snd rty
230+getTTType r = snd <$> check !getEnv r
234231
235232||| Split a pair into its projections, binding them in the context
236233||| with the supplied names. A special case of Coq's `inversion`.
@@ -259,7 +256,6 @@ unproduct tm =
259256 try (unproduct (Var n1))
260257 try (unproduct (Var n2))
261258
262−
263259||| A special-purpose tactic that attempts to solve a goal using
264260||| `Refl`. This is useful for ensuring that goals in fact are trivial
265261||| when developing or testing other tactics; otherwise, consider
@@ -275,36 +271,46 @@ reflexivity =
275271 , TextPart "is not applicable."
276272 ]
277273
278−||| Attempt to swap the sides of equality in a goal.
274+||| Attempt to swap the sides of equality in a goal. If the goal is `x = y`,
275+||| after the invocation the focus will be on a hole of type `y = x`.
279276symmetry : Elab ()
280−symmetry = do
281− [_,_,_,_,_] <- apply (Var `{{sym}}) [True, True, True, True, False]
282− | _ => fail [TextPart "Failed while applying", NamePart `{symmetry} ]
283− solve
284− attack
285−
286−||| Swap the sides of an equality and bind the result to supplied name.
287−symmetryIn : Raw -> TTName -> Elab ()
288−symmetryIn t n = do
289− tt <- getTTType t
290− case tt of
291− `((=) {A=~A} {B=~B} ~l ~r) => do
292− af <- forget A
293− bf <- forget B
294− lf <- forget l
295− rf <- forget r
296− let ts = the Raw $ `(sym {a=~af} {b=~bf} {left=~lf} {right=~rf} ~t)
297− tsty <- forget !(getTTType ts)
298− letbind n tsty ts
299− _ => fail [TermPart tt, TextPart "is not an equality"]
300−
301−||| Apply argument term to a function term and bind the result to supplied name.
302−applyIn : Raw -> Raw -> TTName -> Elab ()
303−applyIn f x n = do
304− ftt <- getTTType f
305− case ftt of
306− `(~xty -> ~yty) => do
307− let fx = RApp f x
308− fxty <- forget !(getTTType fx)
309− letbind n fxty fx
310− _ => fail [TermPart ftt, TextPart "is not a function"]
277+symmetry =
278+ do [_,_,_,_,res] <- apply (Var `{{sym}}) [True, True, True, True, False]
279+ | _ => fail [TextPart "Failed while applying", NamePart `{symmetry}]
280+ solve
281+ focus res
282+
283+||| Swap the sides of an equality, saving the result in a `let`-binding.
284+||| Returns the generated name.
285+|||
286+||| @ t the equality proof to swap
287+||| @ hint a hint to use for generating the variable name for the result
288+symmetryAs : (t : Raw) -> (hint : String) -> Elab TTName
289+symmetryAs t hint =
290+ case !(getTTType t) of
291+ `((=) {A=~A} {B=~B} ~l ~r) =>
292+ do af <- forget A
293+ bf <- forget B
294+ lf <- forget l
295+ rf <- forget r
296+ let ts = the Raw $ `(sym {a=~af} {b=~bf} {left=~lf} {right=~rf} ~t)
297+ n <- gensym hint
298+ letbind n !(forget !(getTTType ts)) ts
299+ pure n
300+ tt => fail [TermPart tt, TextPart "is not an equality"]
301+
302+||| Apply a function term to an argument term, saving the result in a
303+||| `let`-binding. Returns the generated name.
304+|||
305+||| @ f the function to apply
306+||| @ x the term to apply to
307+||| @ hint a hint to use for generating the variable name for the result
308+applyAs : (f : Raw) -> (x : Raw) -> (hint : String) -> Elab TTName
309+applyAs f x hint =
310+ case !(getTTType f) of
311+ `(~xty -> ~yty) =>
312+ do let fx = RApp f x
313+ n <- gensym hint
314+ letbind n !(forget !(getTTType fx)) fx
315+ pure n
316+ ftt => fail [TermPart ftt, TextPart "is not a function"]