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.

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

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

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

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

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

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

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

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