run_tacq and by_elabq

This file provides Qq analogues to by_elab and run_tac.

def Qq.termBy_elabq_ : Lean.ParserDescr

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))

def Qq.«tacticRun_tacq_=>_» : Lean.ParserDescr

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.