Qq integration for simprocs

This file adds wrappers for operations relating to simprocs 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

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

@[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 }

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

@[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

@[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

@[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

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

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