Documentation

Lean.Elab.AutoBound

constant Lean.Elab.autoBoundImplicitLocal :

Lean.Option Bool

def Lean.Elab.isValidAutoBoundImplicitName (n : Lean.Name) :

Equations

Lean.Elab.isValidAutoBoundImplicitName n = match n with | Lean.Name.str Lean.Name.anonymous s x => decide (String.length s > 0) && (Lean.isGreek (String.getOp s 0) || Char.isLower (String.getOp s 0)) && Lean.Elab.isValidAutoBoundSuffix s | x => false

def Lean.Elab.isValidAutoBoundLevelName (n : Lean.Name) :

Equations

Lean.Elab.isValidAutoBoundLevelName n = match n with | Lean.Name.str Lean.Name.anonymous s x => decide (String.length s > 0) && Char.isLower (String.getOp s 0) && Lean.Elab.isValidAutoBoundSuffix s | x => false