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

chore: update compiler version

main
Henrik Böving 2022-01-15 15:35:52 +01:00
parent 1edf4bbdab
commit 735bfa35a7
3 changed files with 7 additions and 12 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

7
DocGen4/Hierarchy.lean
View File

@ -11,9 +11,8 @@ namespace DocGen4
open Lean Std Name open Lean Std Name
def getNLevels (name : Name) (levels: Nat) : Name := def getNLevels (name : Name) (levels: Nat) : Name :=
(components.drop (components.length - levels)).reverse.foldl (· ++ ·) Name.anonymous let components := name.components'
where (components.drop (components.length - levels)).reverse.foldl (· ++ ·) Name.anonymous
components := name.components'
inductive Hierarchy where inductive Hierarchy where
| node (name : Name) (isFile : Bool) (children : RBNode Name (λ _ => Hierarchy)) : Hierarchy | node (name : Name) (isFile : Bool) (children : RBNode Name (λ _ => Hierarchy)) : Hierarchy
@ -54,8 +53,6 @@ partial def insert! (h : Hierarchy) (n : Name) : Hierarchy := Id.run $ do
let hn := h.getName let hn := h.getName
let mut cs := h.getChildren let mut cs := h.getChildren
assert! getNumParts hn ≤ getNumParts n
if getNumParts hn + 1 == getNumParts n then if getNumParts hn + 1 == getNumParts n then
match cs.find Name.cmp n with match cs.find Name.cmp n with
| none => | none =>

10
DocGen4/Output/Base.lean
View File

@ -38,14 +38,12 @@ def moduleNameToLink (n : Name) : HtmlM String := do
(←getRoot) ++ (parts.intersperse "/").foldl (· ++ ·) "" ++ ".html" (←getRoot) ++ (parts.intersperse "/").foldl (· ++ ·) "" ++ ".html"
def moduleNameToFile (basePath : FilePath) (n : Name) : FilePath := def moduleNameToFile (basePath : FilePath) (n : Name) : FilePath :=
FilePath.withExtension (basePath / parts.foldl (· / ·) (FilePath.mk ".")) "html" let parts := n.components.map Name.toString
where FilePath.withExtension (basePath / parts.foldl (· / ·) (FilePath.mk ".")) "html"
parts := n.components.map Name.toString
def moduleNameToDirectory (basePath : FilePath) (n : Name) : FilePath := def moduleNameToDirectory (basePath : FilePath) (n : Name) : FilePath :=
basePath / parts.foldl (· / ·) (FilePath.mk ".") let parts := n.components.dropLast.map Name.toString
where basePath / parts.foldl (· / ·) (FilePath.mk ".")
parts := n.components.dropLast.map Name.toString
section Static section Static
def styleCss : String := include_str "./static/style.css" def styleCss : String := include_str "./static/style.css"

2
lean-toolchain
View File

@ -1 +1 @@
leanprover/lean4:nightly-2022-01-04 leanprover/lean4:nightly-2022-01-15