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

chore: update toolchain

main
Henrik Böving 2022-12-22 15:40:34 +01:00
parent f221bbdcff
commit 345036e800
3 changed files with 4 additions and 4 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
DocGen4/Process/Base.lean
View File

@ -166,7 +166,7 @@ inductive DocInfo where
Turns an `Expr` into a pretty printed `CodeWithInfos`. Turns an `Expr` into a pretty printed `CodeWithInfos`.
-/ -/
def prettyPrintTerm (expr : Expr) : MetaM CodeWithInfos := do def prettyPrintTerm (expr : Expr) : MetaM CodeWithInfos := do
let (fmt, infos) ← PrettyPrinter.ppExprWithInfos expr let ⟨fmt, infos⟩ ← PrettyPrinter.ppExprWithInfos expr
let tt := TaggedText.prettyTagged fmt let tt := TaggedText.prettyTagged fmt
let ctx := { let ctx := {
env := ← getEnv env := ← getEnv
@ -177,7 +177,7 @@ def prettyPrintTerm (expr : Expr) : MetaM CodeWithInfos := do
fileMap := default, fileMap := default,
ngen := ← getNGen ngen := ← getNGen
} }
pure <| tagExprInfos ctx infos tt pure <| tagCodeInfos ctx infos tt
def isInstance (declName : Name) : MetaM Bool := do def isInstance (declName : Name) : MetaM Bool := do
pure <| (instanceExtension.getState (←getEnv)).instanceNames.contains declName pure <| (instanceExtension.getState (←getEnv)).instanceNames.contains declName

2
lake-manifest.json
View File

@ -22,7 +22,7 @@
{"git": {"git":
{"url": "https://github.com/hargonix/LeanInk", {"url": "https://github.com/hargonix/LeanInk",
"subDir?": null, "subDir?": null,
"rev": "9f3101452135964ac9107ec8e9910bfd14022bbc", "rev": "2447df5cc6e48eb965c3c3fba87e46d353b5e9f1",
"name": "leanInk", "name": "leanInk",
"inputRev?": "doc-gen"}}, "inputRev?": "doc-gen"}},
{"git": {"git":

2
lean-toolchain
View File

@ -1 +1 @@
leanprover/lean4:nightly-2022-12-05 leanprover/lean4:nightly-2022-12-16