def Lean.addNoncomputable (env : Lean.Environment) (declName : Lean.Name) :
Mark in the environment extension that the given declaration has been declared by the user as
- Lean.addNoncomputable env declName = Lean.TagDeclarationExtension.tag Lean.noncomputableExt env declName
def Lean.isNoncomputable (env : Lean.Environment) (declName : Lean.Name) :
Return true iff the user has declared the given declaration as
Remark: we use this function only for introspection. It is currently not used by the code generator.
- Lean.isNoncomputable env declName = Lean.TagDeclarationExtension.isTagged Lean.noncomputableExt env declName