← Copula mathematical handbook

@[cbv_opaque] Attribute and Extension

Scoped set of declaration names that cbv should not unfold. Supports erase to remove a declaration from the set within a scope.

@[reducible, inline]

abbrev Lean.Meta.Tactic.Cbv.CbvOpaqueExtension : Type

Equations

• Lean.Meta.Tactic.Cbv.CbvOpaqueExtension = Lean.SimpleScopedEnvExtension Lean.Name (Std.HashSet Lean.Name)

opaque Lean.Meta.Tactic.Cbv.cbvOpaqueExt : CbvOpaqueExtension

def Lean.Meta.Tactic.Cbv.cbvOpaque : CoreM (Std.HashSet Name)

Equations

• Lean.Meta.Tactic.Cbv.cbvOpaque = do let __do_lift ← Lean.getEnv pure (Lean.ScopedEnvExtension.getState Lean.Meta.Tactic.Cbv.cbvOpaqueExt __do_lift)

def Lean.Meta.Tactic.Cbv.isCbvOpaque (name : Name) : CoreM Bool

Equations

• Lean.Meta.Tactic.Cbv.isCbvOpaque name = do let __do_lift ← Lean.getEnv pure ((Lean.ScopedEnvExtension.getState Lean.Meta.Tactic.Cbv.cbvOpaqueExt __do_lift).contains name)