r
/
bookshelf-doc
mirror of https://github.com/jrpotter/bookshelf-doc
1
Fork 0
Code Issues Packages Projects Releases Wiki Activity

feat: tag abbrevs

main
Henrik Böving 2022-02-06 17:28:56 +01:00
parent c2d18fe3b1
commit 27f8b50763
1 changed files with 10 additions and 5 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

15
DocGen4/Process.lean
View File

@ -340,16 +340,21 @@ def getKind : DocInfo → String
| structureInfo _ => "structure" | structureInfo _ => "structure"
| classInfo _ => "class" | classInfo _ => "class"
open DefinitionSafety in
def getKindDescription : DocInfo → String def getKindDescription : DocInfo → String
| axiomInfo i => if i.isUnsafe then "unsafe axiom" else "axiom" | axiomInfo i => if i.isUnsafe then "unsafe axiom" else "axiom"
| theoremInfo _ => "theorem" | theoremInfo _ => "theorem"
| opaqueInfo i => | opaqueInfo i =>
match i.unsafeInformation with match i.unsafeInformation with
| safe => "constant" | DefinitionSafety.safe => "constant"
| «unsafe» => "unsafe constant" | DefinitionSafety.unsafe => "unsafe constant"
| «partial» => "partial def" | DefinitionSafety.partial => "partial def"
| definitionInfo i => if i.isUnsafe then "unsafe def" else "def" | definitionInfo i =>
if i.hints.isAbbrev then
"abbrev"
else if i.isUnsafe then
"unsafe def"
else
"def"
| instanceInfo i => if i.isUnsafe then "unsafe instance" else "instance" | instanceInfo i => if i.isUnsafe then "unsafe instance" else "instance"
| inductiveInfo i => if i.isUnsafe then "unsafe inductive" else "inductive" | inductiveInfo i => if i.isUnsafe then "unsafe inductive" else "inductive"
| structureInfo _ => "structure" | structureInfo _ => "structure"