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

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

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

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