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

chore: Update compiler and fix minor breaking change

main
Henrik Böving 2021-12-11 14:26:32 +01:00
parent e9a9e17439
commit c2da7afd76
2 changed files with 2 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
DocGen4/Process.lean
View File

@ -96,7 +96,7 @@ def prettyPrintTerm (expr : Expr) : MetaM Syntax := do
def Info.ofConstantVal (v : ConstantVal) : MetaM Info := do def Info.ofConstantVal (v : ConstantVal) : MetaM Info := do
let env ← getEnv let env ← getEnv
let type ← prettyPrintTerm v.type let type ← prettyPrintTerm v.type
let doc := findDocString? env v.name let doc ← findDocString? env v.name
match ←findDeclarationRanges? v.name with match ←findDeclarationRanges? v.name with
-- TODO: Maybe selection range is more relevant? Figure this out in the future -- TODO: Maybe selection range is more relevant? Figure this out in the future
| some range => return Info.mk ⟨v.name, type⟩ doc range.range | some range => return Info.mk ⟨v.name, type⟩ doc range.range

2
lean-toolchain
View File

@ -1 +1 @@
leanprover/lean4:nightly-2021-11-26 leanprover/lean4:nightly-2021-12-10