def EvalAuto.Name.canBeFilename (n : Lean.Name) : Bool

Whether a name is a valid filename

Equations

• One or more equations did not get rendered due to their size.

def EvalAuto.Name.uniqRepr (n : Lean.Name) : String

Unique string representation of names, where it is ensured that \n does not occur A . is appended to the end of the name We use "\d" to represent ".", "\n" to represent "\n", "\\" to represent "\" To distinguish mkStr and mkNum, we prepend \ to all mkNum fields

Equations

• One or more equations did not get rendered due to their size.

def EvalAuto.Name.parseUniqRepr (n : String) : Lean.Name

Parsing unique representation of names, see Name.uniqRepr

Equations

• One or more equations did not get rendered due to their size.

def EvalAuto.NameArray.repr (ns : Array Lean.Name) : String

Each name in the array is represented using Name.uniqRepr Names are separated using \n. A \n is further appended to the end of the last name.

Equations

• EvalAuto.NameArray.repr ns = String.join (Array.map (fun (n : Lean.Name) => EvalAuto.Name.uniqRepr n ++ "\n") ns).toList

def EvalAuto.NameArray.parse (repr : String) : Array Lean.Name

Equations

• EvalAuto.NameArray.parse repr = { toList := (List.map EvalAuto.Name.parseUniqRepr (repr.splitOn "\n")).dropLast }

def EvalAuto.NameArray.save (ns : Array Lean.Name) (fname : String) : IO Unit

Equations

• EvalAuto.NameArray.save ns fname = do let fd ← IO.FS.Handle.mk { toString := fname } IO.FS.Mode.write fd.putStr (EvalAuto.NameArray.repr ns)

def EvalAuto.NameArray.load (fname : String) : IO (Array Lean.Name)

Equations

• EvalAuto.NameArray.load fname = do let fd ← IO.FS.Handle.mk { toString := fname } IO.FS.Mode.read let __do_lift ← fd.readToEnd pure (EvalAuto.NameArray.parse __do_lift)