# Qq integration for `simproc`s #

This file adds wrappers for operations relating to `simproc`s in the `Lean.Meta.Simp` namespace.

It can be used as

    simproc_decl some_proc (some_pattern) := Meta.Simp.Simproc.ofQ fun u α e => do
      sorry

instead of the usual

    simproc_decl some_proc (some_pattern) := fun e => do
      sorry

source
def Lean.Meta.Simp.ResultQ {u : Level} {α : Q(Sort u)} (_e : Q(«$α»)) :
Type

A copy of `Meta.Simp.Result` with explicit types.

Equations

- Lean.Meta.Simp.ResultQ _e = Lean.Meta.Simp.Result

Instances For

source
@[inline]
def Lean.Meta.Simp.ResultQ.mk {u : Level} {α : Q(Sort u)} {e : Q(«$α»)} (expr : Q(«$α»)) (proof? : Option Q(«$e» = «$expr»)) (cache : Bool := true) :
ResultQ e

A copy of `Meta.Simp.Result.mk` with explicit types.

Equations

- Lean.Meta.Simp.ResultQ.mk expr proof? cache = { expr := expr, proof? := proof?, cache := cache }

Instances For

source
def Lean.Meta.Simp.StepQ {u : Level} {α : Q(Sort u)} (_e : Q(«$α»)) :
Type

A copy of `Meta.Simp.Step` with explicit types.

Equations

- Lean.Meta.Simp.StepQ _e = Lean.Meta.Simp.Step

Instances For

source
@[inline]
def Lean.Meta.Simp.StepQ.done {u : Level} {α : Q(Sort u)} {e : Q(«$α»)} (r : ResultQ e) :
StepQ e

For `pre` procedures, it returns the result without visiting any subexpressions.

For `post` procedures, it returns the result.

Equations

- Lean.Meta.Simp.StepQ.done r = Lean.Meta.Simp.Step.done r

Instances For

source
@[inline]
def Lean.Meta.Simp.StepQ.visit {u : Level} {α : Q(Sort u)} {e : Q(«$α»)} (r : ResultQ e) :
StepQ e

For `pre` procedures, the resulting expression is passed to `pre` again.

For `post` procedures, the resulting expression is passed to `pre` again IF `Simp.Config.singlePass := false` and resulting expression is not equal to initial expression.

Equations

- Lean.Meta.Simp.StepQ.visit r = Lean.Meta.Simp.Step.visit r

Instances For

source
@[inline]
def Lean.Meta.Simp.StepQ.continue {u : Level} {α : Q(Sort u)} {e : Q(«$α»)} (r : Option (ResultQ e) := none) :
StepQ e

For `pre` procedures, continue transformation by visiting subexpressions, and then executing `post` procedures.

For `post` procedures, this is equivalent to returning `visit`.

Equations

- Lean.Meta.Simp.StepQ.continue r = Lean.Meta.Simp.Step.continue r

Instances For

source
@[reducible, inline]
abbrev Lean.Meta.Simp.SimprocQ :
Type

A copy of `Lean.Meta.Simproc` with explicit types.

See `Simproc.ofQ` to construct terms of this type.

Equations

- Lean.Meta.Simp.SimprocQ = ((u : Lean.Level) → (α : Q(Sort u)) → (e : Q(«$α»)) → Lean.Meta.SimpM (Lean.Meta.Simp.StepQ e))

Instances For

source
@[inline]
def Lean.Meta.Simp.Simproc.ofQ (proc : SimprocQ) :
Simproc

Build a simproc with Qq-enabled typechecking of inputs and outputs.

This calls `inferTypeQ` on the expression and passes the arguments to `proc`.

Equations

- Lean.Meta.Simp.Simproc.ofQ proc e = do let __discr ← liftM (Qq.inferTypeQ e) match __discr with | ⟨u, ⟨α, e⟩⟩ => proc u α e

Instances For