book/TPiL.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Imports (13)
  1. def versionString line 21 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Verso.Doc.Elab.RoleExpander

    Proof uses: Array, Verso.Doc.Arg, Lean.TSyntaxArray, List.cons, Lean.SyntaxNodeKind, Lean.Name.mkStr1, List.nil, versionString.match_1, Verso.Doc.Elab.DocElabM, Lean.TSyntax, Unit, Bind.bind, String, liftM, EIO, IO.Error, IO, IO.FS.readFile, System.FilePath.mk, String.Slice.copy and 25 more

    22 instances, coercions and auxiliary constants left out.