Lean4
/-- Runs `mx` in a context where all local `Subsingleton` and `IsEmpty` instances
have associated `FastSubsingleton` and `FastIsEmpty` instances.
The function passed to `mx` eliminates these instances from expressions,
since they are only locally valid inside this context.
-/
def withSubsingletonAsFast {α : Type} [Inhabited α] (mx : (Expr → Expr) → MetaM α) : MetaM α := do
let insts1 := (← getLocalInstances).filter fun inst => inst.className == ``Subsingleton
let insts2 := (← getLocalInstances).filter fun inst => inst.className == ``IsEmpty
let mkInst (f : Name) (inst : Expr) : MetaM Expr := do
forallTelescopeReducing (← inferType inst) fun args _ => do
mkLambdaFVars args <| ← mkAppOptM f #[none, mkAppN inst args]
let vals :=
(← insts1.mapM fun inst => mkInst ``FastSubsingleton.mk inst.fvar) ++
(← insts2.mapM fun inst => mkInst ``FastIsEmpty.mk inst.fvar)
let tys ← vals.mapM inferType
withLocalDeclsD (tys.map fun ty => (`inst, fun _ => pure ty)) fun args =>
withNewLocalInstances args 0 do
let elim (e : Expr) : Expr := e.replaceFVars args vals
mx elim
