run_tacq
and by_elabq
#
This file provides Qq analogues to by_elab
and run_tac
.
by_elabq
is the Qq analogue to by_elab
which allows executing arbitrary TermElabM
code in
place of a term. In contrast to by_elab
, the local context can be directly accessed as quoted
expressions and the return type is Q-annotated.
Example:
def f (x : Prop) [Decidable x] : Int :=
by_elabq
Lean.logInfo x
Lean.logInfo x.ty
return q(if $x then 2 else 3)
See also: run_tacq
.
Equations
- Qq.termBy_elabq_ = Lean.ParserDescr.node `Qq.termBy_elabq_ 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "by_elabq") (Lean.ParserDescr.const `doSeq))
Instances For
run_tacq
is the Qq analogue to run_tac
which allows executing arbitrary TacticM
code.
In contrast to run_tac
, the local context of the main goal can be directly accessed as quoted
expressions. Optionally, the annotated goal can also be saved using the syntax run_tacq $g =>
.
Example:
example (a b : Nat) (h : a = b) : True := by
run_tacq goal =>
let p : Q(Prop) := q($a = $b)
let t ← Lean.Meta.inferType h
Lean.logInfo p
Lean.logInfo <| toString (← Lean.Meta.isDefEq t p)
Lean.logInfo <| toString (← Lean.Meta.isDefEq h.ty p)
Lean.logInfo goal
Lean.logInfo goal.ty
trivial
See also: by_elabq
.
Equations
- One or more equations did not get rendered due to their size.