From f0c4ef534bdb2d8bc18faf95a571c0c52de40b05 Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Wed, 25 Jun 2025 06:30:41 +0200 Subject: [PATCH] chore: adapt to elab branch --- Manual/Classes.lean | 8 +- Manual/Elaboration.lean | 4 +- Manual/Intro.lean | 12 +- Manual/Language/InductiveTypes.lean | 13 +- .../Language/InductiveTypes/Structures.lean | 2 - Manual/Meta/Example.lean | 29 +- Manual/Meta/Tactics.lean | 547 +++++++++++------- Manual/NotationsMacros.lean | 8 +- Manual/NotationsMacros/Delab.lean | 6 +- Manual/RecursiveDefs/WF.lean | 2 +- .../RecursiveDefs/WF/PreprocessExample.lean | 4 +- Manual/Simp.lean | 6 +- Manual/Tactics/Reference.lean | 2 +- Manual/Terms.lean | 35 +- Manual/Types.lean | 10 +- lake-manifest.json | 4 +- lakefile.lean | 2 +- 17 files changed, 406 insertions(+), 288 deletions(-) diff --git a/Manual/Classes.lean b/Manual/Classes.lean index 28fc3c04..21d1ae86 100644 --- a/Manual/Classes.lean +++ b/Manual/Classes.lean @@ -159,7 +159,7 @@ use the command `set_option checkBinderAnnotations false` to disable the check ::::example "Class vs Structure Constructors" A very small algebraic hierarchy can be represented either as structures ({name}`S.Magma`, {name}`S.Semigroup`, and {name}`S.Monoid` below), a mix of structures and classes ({name}`C1.Monoid`), or only using classes ({name}`C2.Magma`, {name}`C2.Semigroup`, and {name}`C2.Monoid`): -````lean +```lean namespace S structure Magma (α : Type u) where op : α → α → α @@ -192,7 +192,7 @@ class Monoid (α : Type u) extends Semigroup α where ident_left : ∀ x, op ident x = x ident_right : ∀ x, op x ident = x end C2 -```` +``` {name}`S.Monoid.mk` and {name}`C1.Monoid.mk` have identical signatures, because the parent of the class {name}`C1.Monoid` is not itself a class: @@ -258,7 +258,7 @@ Two instances of the same class with the same parameters are not necessarily ide ::::example "Instances are Not Unique" This implementation of binary heap insertion is buggy: -````lean +```lean structure Heap (α : Type u) where contents : Array α deriving Repr @@ -275,7 +275,7 @@ def Heap.bubbleUp [Ord α] (i : Nat) (xs : Heap α) : Heap α := def Heap.insert [Ord α] (x : α) (xs : Heap α) : Heap α := let i := xs.contents.size {xs with contents := xs.contents.push x}.bubbleUp i -```` +``` The problem is that a heap constructed with one {name}`Ord` instance may later be used with another, leading to the breaking of the heap invariant. diff --git a/Manual/Elaboration.lean b/Manual/Elaboration.lean index 24cbf481..17f7dab0 100644 --- a/Manual/Elaboration.lean +++ b/Manual/Elaboration.lean @@ -139,10 +139,10 @@ When interacting with Lean code, much more information is needed than when simpl For example, Lean's interactive environment can be used to view the types of selected expressions, to step through all the intermediate states of a proof, to view documentation, and highlight all occurrences of a bound variable. The information necessary to use Lean interactively is stored in a side table called the {deftech}_info trees_ during elaboration. -````lean (show := false) +```lean (show := false) open Lean.Elab (Info) deriving instance TypeName for Unit -```` +``` Info trees relate metadata to the user's original syntax. diff --git a/Manual/Intro.lean b/Manual/Intro.lean index 13290ee1..4fcae820 100644 --- a/Manual/Intro.lean +++ b/Manual/Intro.lean @@ -73,19 +73,19 @@ tag := "code-samples" This document contains many Lean code examples. They are formatted as follows: -````lean +```lean def hello : IO Unit := IO.println "Hello, world!" -```` +``` Compiler output (which may be errors, warnings, or just information) is shown both in the code and separately: -````lean (name := output) (error := true) +```lean (name := output) (error := true) #eval s!"The answer is {2 + 2}" theorem bogus : False := by sorry example := Nat.succ "two" -```` +``` Informative output, such as the result of {keywordOf Lean.Parser.Command.eval}`#eval`, is shown like this: ```leanOutput output (severity := information) @@ -183,7 +183,7 @@ tag := "reference-boxes" Definitions, inductive types, syntax formers, and tactics have specific descriptions. These descriptions are marked as follows: -::::keepEnv + ```lean /-- Evenness: a number is even if it can be evenly divided by two. @@ -197,7 +197,7 @@ inductive Even : Nat → Prop where {docstring Even} -:::: + # Open-Source Licenses %%% diff --git a/Manual/Language/InductiveTypes.lean b/Manual/Language/InductiveTypes.lean index ab9ca1a5..dd896470 100644 --- a/Manual/Language/InductiveTypes.lean +++ b/Manual/Language/InductiveTypes.lean @@ -305,12 +305,13 @@ Constructors can be invoked anonymously by enclosing their explicit arguments in ::::example "Anonymous constructors" -:::keepEnv + ```lean (show:=false) -axiom α : Type +variable {α : Type u} ``` + The type {lean}`AtLeastOne α` is similar to `List α`, except there's always at least one element present: -::: + ```lean inductive AtLeastOne (α : Type u) : Type u where @@ -366,9 +367,9 @@ tag := "inductive-types-runtime-special-support" Not every inductive type is represented as indicated here—some inductive types have special support from the Lean compiler: :::keepEnv -````lean (show := false) +```lean (show := false) axiom α : Prop -```` +``` * The representation of the fixed-width integer types {lean}`UInt8`, …, {lean}`UInt64`, {lean}`Int8`, …, {lean}`Int64`, and {lean}`USize` depends on the whether the code is compiled for a 32- or 64-bit architecture. Fixed-width integer types that are strictly smaller than the architecture's pointer type are stored unboxed by setting the lowest bit of a pointer to `1`. @@ -473,7 +474,7 @@ The memory order of the fields is derived from the types and order of the fields * Fields of type {lean}`USize` * Other scalar fields, in decreasing order by size -Within each group the fields are ordered in declaration order. **Warning**: Trivial wrapper types still count toward a field being treated as non-scalar for this purpose. +Within each group the fields are ordered in declaration order. *Warning*: Trivial wrapper types still count toward a field being treated as non-scalar for this purpose. * To access fields of the first kind, use {c}`lean_ctor_get(val, i)` to get the `i`th non-scalar field. * To access {lean}`USize` fields, use {c}`lean_ctor_get_usize(val, n+i)` to get the {c}`i`th `USize` field and {c}`n` is the total number of fields of the first kind. diff --git a/Manual/Language/InductiveTypes/Structures.lean b/Manual/Language/InductiveTypes/Structures.lean index 20038b25..ce3d7a4d 100644 --- a/Manual/Language/InductiveTypes/Structures.lean +++ b/Manual/Language/InductiveTypes/Structures.lean @@ -507,7 +507,6 @@ example (t : Triple α) : t.fst = t.toPair.fst := rfl :::: :::: example "No structure subtyping" -:::keepEnv Given these definitions of even numbers, even prime numbers, and a concrete even prime: ```lean structure EvenNumber where @@ -543,7 +542,6 @@ but is expected to have type EvenNumber : Type ``` because values of type {name}`EvenPrime` are not also values of type {name}`EvenNumber`. -::: :::: diff --git a/Manual/Meta/Example.lean b/Manual/Meta/Example.lean index 10ec229f..a4a84030 100644 --- a/Manual/Meta/Example.lean +++ b/Manual/Meta/Example.lean @@ -45,13 +45,13 @@ def prioritizedElab [Monad m] (prioritize : α → m Bool) (act : α → m β) def isLeanBlock : TSyntax `block → CoreM Bool | `(block|```$nameStx:ident $_args*|$_contents:str```) => do - let name ← realizeGlobalConstNoOverloadWithInfo nameStx + let name ← realizeGlobalConstNoOverload nameStx return name == ``Verso.Genre.Manual.InlineLean.lean | _ => pure false -@[directive_expander «example»] -def «example» : DirectiveExpander +@[directive_elab «example»] +def «example» : DirectiveElab | args, contents => do let cfg ← ExampleConfig.parse.run args @@ -65,12 +65,23 @@ def «example» : DirectiveExpander -- Elaborate Lean blocks first, so inlines in prior blocks can refer to them let blocks ← if cfg.keep then - prioritizedElab (isLeanBlock ·) elabBlock contents + prioritizedElab (isLeanBlock ·) elabBlock' contents else - withoutModifyingEnv <| prioritizedElab (isLeanBlock ·) elabBlock contents + InlineLean.withIsolatedExamplesEnv <| prioritizedElab (isLeanBlock ·) elabBlock' contents + + let it ← DocElabM.inlineType + let bt ← DocElabM.blockType + + let description ← description.mapM (Term.elabTerm · (some it)) + -- Examples are represented using the first block to hold the description. Storing it in the JSON -- entails repeated (de)serialization. - pure #[← ``(Block.other (Block.example $(quote cfg.tag)) #[Block.para #[$description,*], $blocks,*])] + let g ← DocElabM.genreExpr + let exampleBlock : Expr := .app (.const ``Block.example []) (toExpr cfg.tag) + let descr : Expr := mkApp2 (.const ``Block.para []) g (← Meta.mkArrayLit it description.toList) + let blocks := #[descr] ++ blocks + return mkApp3 (.const ``Block.other []) g exampleBlock (← Meta.mkArrayLit bt blocks.toList) + @[block_extension «example»] def example.descr : BlockDescr where @@ -147,16 +158,14 @@ r#".example { ] -def Block.keepEnv : Block where - name := `Manual.example - -- TODO rename to `withoutModifyingEnv` or something more clear @[directive_expander keepEnv] def keepEnv : DirectiveExpander | args, contents => do let () ← ArgParse.done.run args PointOfInterest.save (← getRef) "keepEnv" (kind := .package) - withoutModifyingEnv <| withSaveInfoContext <| contents.mapM elabBlock + InlineLean.withIsolatedExamplesEnv <| + withSaveInfoContext <| contents.mapM elabBlock @[block_extension keepEnv] diff --git a/Manual/Meta/Tactics.lean b/Manual/Meta/Tactics.lean index 275096db..ae7744f8 100644 --- a/Manual/Meta/Tactics.lean +++ b/Manual/Meta/Tactics.lean @@ -25,11 +25,173 @@ open Verso.Genre.Manual.InlineLean.Scopes (runWithOpenDecls runWithVariables) open SubVerso.Highlighting open SubVerso.Examples.Messages +def Block.proofState (tag : Option String) (hl : Array (Highlighted.Goal Highlighted)) : Block where + name := `Manual.proofState + data := ToJson.toJson (tag, hl) + +structure ProofStateOptions where + tag : Option String := none + + +def ProofStateOptions.parse [Monad m] [MonadInfoTree m] [MonadLiftT CoreM m] [MonadEnv m] [MonadError m] : ArgParse m ProofStateOptions := + ProofStateOptions.mk <$> .named `tag .string true + + +open Lean.Parser in +/-- +Show a proof state in the text. The proof goal is expected as a documentation comment immediately +prior to tactics. +-/ +@[code_block_expander proofState] +def proofState : CodeBlockExpander + | args, str => InlineLean.usingExamplesEnv do + let opts ← ProofStateOptions.parse.run args + let altStr ← parserInputString str + let p := + node nullKind <| + andthen ⟨{}, whitespace⟩ <| + andthen termParser <| + andthen ⟨{}, whitespace⟩ <| + andthen ":=" <| andthen ⟨{}, whitespace⟩ <| andthen "by" <| + andthen ⟨{}, whitespace⟩ <| + andthen (andthen {fn := (fun _ => (·.pushSyntax (mkIdent `tacticSeq)))} (parserOfStack 0)) <| + optional <| + andthen ⟨{}, whitespace⟩ <| + Command.docComment + match runParser (← getEnv) (← getOptions) p altStr (← getFileName) with + | .error es => + for (pos, msg) in es do + log (severity := .error) (mkErrorStringWithPos "" pos msg) + throwErrorAt str "Failed to parse config (expected goal term, followed by ':=', 'by', and tactics, with optional docstring)" + | .ok stx => + let goalStx := stx[0] + let tacticStx := stx[4] + let desired := + match stx[5][0] with + | .missing => none + | other => some (⟨other⟩ : TSyntax `Lean.Parser.Command.docComment) + let goalExpr ← runWithOpenDecls <| runWithVariables fun _ => Elab.Term.elabTerm goalStx none + let mv ← Meta.mkFreshExprMVar (some goalExpr) + let Expr.mvar mvarId := mv + | throwError "Not an mvar!" + let (remainingGoals, infoTree) ← withInfoTreeContext (mkInfoTree := mkInfoTree `proofState (← getRef)) do + Tactic.run mvarId <| + withoutTacticIncrementality true <| + withTacticInfoContext tacticStx do + evalTactic tacticStx + synthesizeSyntheticMVars (postpone := .no) + let ci : ContextInfo := { + env := ← getEnv, fileMap := ← getFileMap, ngen := ← getNGen, + mctx := ← getMCtx, options := ← getOptions, + currNamespace := ← getCurrNamespace, openDecls := ← getOpenDecls + } + let hlState ← highlightProofState ci remainingGoals (PersistentArray.empty.push infoTree) + let st := goalsToMessageData remainingGoals + --logInfoAt proofPrefix st1 + let stStr ← (← addMessageContext st).toString + if let some s := desired then + if normalizeMetavars stStr.trim != normalizeMetavars s.getDocString.trim then + logErrorAt s m!"Expected: {indentD stStr}\n\nGot: {indentD s.getDocString}" + Verso.Doc.Suggestion.saveSuggestion s (stStr.take 30 ++ "…") ("/--\n" ++ stStr ++ "\n-/\n") + pure #[← `(Doc.Block.other (Block.proofState $(quote opts.tag) $(quote hlState)) #[Doc.Block.code $(quote stStr)])] + +where + mkInfoTree (elaborator : Name) (stx : Syntax) (trees : PersistentArray InfoTree) : DocElabM InfoTree := do + let tree := InfoTree.node (Info.ofCommandInfo { elaborator, stx }) trees + let ctx := PartialContextInfo.commandCtx { + env := ← getEnv, fileMap := ← getFileMap, mctx := {}, currNamespace := ← getCurrNamespace, + openDecls := ← getOpenDecls, options := ← getOptions, ngen := ← getNGen + } + return InfoTree.context ctx tree + + modifyInfoTrees {m} [Monad m] [MonadInfoTree m] (f : PersistentArray InfoTree → PersistentArray InfoTree) : m Unit := + modifyInfoState fun s => { s with trees := f s.trees } + + -- TODO - consider how to upstream this + withInfoTreeContext {m α} [Monad m] [MonadInfoTree m] [MonadFinally m] (x : m α) (mkInfoTree : PersistentArray InfoTree → m InfoTree) : m (α × InfoTree) := do + let treesSaved ← getResetInfoTrees + MonadFinally.tryFinally' x fun _ => do + let st ← getInfoState + let tree ← mkInfoTree st.trees + modifyInfoTrees fun _ => treesSaved.push tree + pure tree + + + + +def proofStateStyle := r#" +.hl.lean.tactic-view { + white-space: collapse; +} +.hl.lean.tactic-view .tactic-state { + display: block; + left: 0; + padding: 0; + border: none; +} +.hl.lean.tactic-view .tactic-state .goal { + margin-top: 1em; + margin-bottom: 1em; + display: block; +} +.hl.lean.tactic-view .tactic-state .goal:first-child { + margin-top: 0.25em; +} +.hl.lean.tactic-view .tactic-state .goal:last-child { + margin-bottom: 0.25em; +} + + +"# + + + +@[block_extension Manual.proofState] +def proofState.descr : BlockDescr where + traverse id data content := do + match FromJson.fromJson? data (α := Option String × Array (Highlighted.Goal Highlighted)) with + | .error e => logError s!"Error deserializing proof state info: {e}"; pure none + | .ok (none, _) => pure none + | .ok (some t, v) => + let path ← (·.path) <$> read + let _tag ← Verso.Genre.Manual.externalTag id path t + pure <| some <| Block.other {Block.proofState none v with id := some id, data := ToJson.toJson (α := (Option String × _)) (none, v)} content + + toTeX := none + extraCss := [highlightingStyle, proofStateStyle] + extraJs := [highlightingJs] + extraJsFiles := [("popper.js", popper), ("tippy.js", tippy)] + extraCssFiles := [("tippy-border.css", tippy.border.css)] + toHtml := + open Verso.Output.Html in + some <| fun _ _ id data _ => do + match FromJson.fromJson? (α := Option Tag × Array (Highlighted.Goal Highlighted)) data with + | .error err => + HtmlT.logError <| "Couldn't deserialize proof state while rendering HTML: " ++ err + pure .empty + | .ok (_, goals) => + let xref ← HtmlT.state + let idAttr := xref.htmlId id + + pure {{ +
+
+ {{← if goals.isEmpty then + pure {{"All goals completed! 🐙"}} + else + .seq <$> goals.mapIndexedM (fun ⟨i, _⟩ x => withCollapsedSubgoals .never <| x.toHtml (·.toHtml) i)}} +
+
+ }} + +deriving instance ToExpr for GuardMsgs.WhitespaceMode + structure TacticOutputConfig where «show» : Bool := true severity : Option MessageSeverity summarize : Bool whitespace : GuardMsgs.WhitespaceMode +deriving ToExpr def TacticOutputConfig.parser [Monad m] [MonadInfoTree m] [MonadLiftT CoreM m] [MonadEnv m] [MonadError m] : ArgParse m TacticOutputConfig := TacticOutputConfig.mk <$> @@ -217,14 +379,14 @@ structure TacticExampleContext where initialize tacticExampleCtx : Lean.EnvExtension (Option TacticExampleContext) ← Lean.registerEnvExtension (pure none) -def startExample [Monad m] [MonadEnv m] [MonadError m] [MonadQuotation m] [MonadRef m] : m Unit := do +def startExample [Monad m] [MonadEnv m] [MonadError m] [MonadLiftT CoreM m] [MonadQuotation m] [MonadRef m] : m Unit := do match tacticExampleCtx.getState (← getEnv) with | some _ => throwError "Can't initialize - already in a context" | none => - let preName ← mkFreshIdent (← getRef) - let tacticName ← mkFreshIdent (← getRef) - let postName ← mkFreshIdent (← getRef) - let outputSeverityName ← mkFreshIdent (← getRef) + let preName := mkIdentFrom (← getRef) (← mkFreshUserName `preState) + let tacticName := mkIdentFrom (← getRef) (← mkFreshUserName `tactic) + let postName := mkIdentFrom (← getRef) (← mkFreshUserName `postState) + let outputSeverityName := mkIdentFrom (← getRef) (← mkFreshUserName `severity) modifyEnv fun env => tacticExampleCtx.setState env (some {preName, tacticName, postName, outputSeverityName}) @@ -271,7 +433,7 @@ def saveOutput [Monad m] [MonadEnv m] [MonadLog m] [MonadRef m] [MonadError m] [ | some st => match st.output with | none => - modifyEnv fun env => tacticExampleCtx.setState env (some {st with output := (output, options)}) + modifyEnv fun env => tacticExampleCtx.setState env (some {st with output := some (output, options)}) | some _ => logErrorAt (← getRef) "Expected output already specified" return st.outputSeverityName @@ -289,40 +451,52 @@ def savePost [Monad m] [MonadEnv m] [MonadLog m] [MonadRef m] [MonadError m] [Ad return st.postName -def endExample (body : TSyntax `term) : DocElabM (TSyntax `term) := do +def endExampleSetup : DocElabM Unit := do match tacticExampleCtx.getState (← getEnv) with - | none => throwErrorAt body "Can't end examples - never started" + | none => throwError "Can't end examples - never started" | some {goal, setup, pre, preName, tactic, tacticName, post, postName, output, outputSeverityName} => modifyEnv fun env => tacticExampleCtx.setState env none let some goal := goal - | throwErrorAt body "No goal specified" + | throwError "No goal specified" let some setup := setup - | throwErrorAt body "No setup specified" + | throwError "No setup specified" let some pre := pre - | throwErrorAt body "No pre-state specified" + | throwError "No pre-state specified" let some tactic := tactic - | throwErrorAt body "No tactic specified" + | throwError "No tactic specified" let some post := post - | throwErrorAt body "No post-state specified" + | throwError "No post-state specified" let (hlPre, hlPost, hlTactic, outputSeverity) ← checkTacticExample' goal setup tactic pre post output - `(let $preName : Array (Highlighted.Goal Highlighted) := $(quote hlPre) - let $postName : Array (Highlighted.Goal Highlighted) := $(quote hlPost) - let $tacticName : Highlighted := $(quote hlTactic) - let $outputSeverityName : MessageSeverity := $(quote outputSeverity) - $body) - -@[directive_expander tacticExample] -def tacticExample : DirectiveExpander - | args, blocks => do - ArgParse.done.run args - startExample - let body ← blocks.mapM elabBlock - let body' ← `(Verso.Doc.Block.concat #[$body,*]) >>= endExample - pure #[body'] + let goalsType : Expr := .app (.const ``Array [0]) (.app (.const ``Highlighted.Goal [0]) (.const ``Highlighted [])) + addAndCompile <| .defnDecl { + name := preName.getId, levelParams := [], type := goalsType, + value := toExpr hlPre, hints := .opaque, safety := .safe + } + addAndCompile <| .defnDecl { + name := postName.getId, levelParams := [], type := goalsType, + value := toExpr hlPost, hints := .opaque, safety := .safe + } + addAndCompile <| .defnDecl { + name := tacticName.getId, levelParams := [], type := .const ``Highlighted [], + value := toExpr hlTactic, hints := .opaque, safety := .safe + } + addAndCompile <| .defnDecl { + name := outputSeverityName.getId, levelParams := [], type := .const ``MessageSeverity [], + value := toExpr outputSeverity, hints := .opaque, safety := .safe + } + let env ← getEnv + let some _ := env.find? preName.getId + | throwError "Didn't define {preName}" + let some _ := env.find? postName.getId + | throwError "Didn't define {postName}" + let some _ := env.find? tacticName.getId + | throwError "Didn't define {tacticName}" + let some _ := env.find? outputSeverityName.getId + | throwError "Didn't define {outputSeverityName}" structure TacticGoalConfig where «show» : Bool @@ -330,8 +504,8 @@ structure TacticGoalConfig where def TacticGoalConfig.parse [Monad m] [MonadInfoTree m] [MonadLiftT CoreM m] [MonadEnv m] [MonadError m] : ArgParse m TacticGoalConfig := TacticGoalConfig.mk <$> ((·.getD true) <$> .named `show .bool true) -@[role_expander goal] -def goal : RoleExpander +@[role_elab goal] +def goal : RoleElab | args, inlines => do let config ← TacticGoalConfig.parse.run args let #[arg] := inlines @@ -359,12 +533,14 @@ def goal : RoleExpander -- TODO msgs let hls := (← highlight stx #[] (PersistentArray.empty.push tree)) + let g ← DocElabM.genreExpr if config.show then -- Just emit a normal Lean node - no need to do anything special with the rendered result - pure #[← ``(Inline.other (Verso.Genre.Manual.InlineLean.Inline.lean $(quote hls)) #[Inline.code $(quote term.getString)])] + let blockType := mkApp (.const ``InlineLean.Inline.lean []) (toExpr hls) + pure <| mkApp3 (.const ``Inline.other []) g blockType (← DocElabM.inlineArray #[mkApp2 (.const ``Inline.code []) g (mkStrLit term.getString)]) else - pure #[] + pure <| mkApp2 (.const ``Inline.concat []) g (← DocElabM.inlineArray #[]) where mkInfoTree (elaborator : Name) (stx : Syntax) (trees : PersistentArray InfoTree) : DocElabM InfoTree := do let tree := InfoTree.node (Info.ofCommandInfo { elaborator, stx }) trees @@ -388,8 +564,8 @@ where open Lean.Parser in -@[code_block_expander setup] -def setup : CodeBlockExpander +@[code_block_elab setup] +def setup : CodeBlockElab | args, str => do let () ← ArgParse.done.run args @@ -403,25 +579,38 @@ def setup : CodeBlockExpander throwErrorAt str "Failed to parse setup" | .ok stx => saveSetup stx - pure #[] + let g ← DocElabM.genreExpr + pure <| mkApp2 (.const ``Block.concat []) g (← DocElabM.blockArray #[]) open Lean.Parser in -@[code_block_expander tacticOutput] -def tacticOutput : CodeBlockExpander +@[code_block_elab tacticOutput] +def tacticOutput : CodeBlockElab | args, str => do let opts ← TacticOutputConfig.parser.run args let outputSeverityName ← saveOutput str opts + let g ← DocElabM.genreExpr + if opts.show then - return #[← `(Block.other {Verso.Genre.Manual.InlineLean.Block.leanOutput with data := ToJson.toJson ($outputSeverityName, $(quote str.getString), $(quote opts.summarize))} #[Block.code $(quote str.getString)])] + let t := mkApp2 (.const ``Prod [0, 0]) (.const ``MessageSeverity []) (mkApp2 (.const ``Prod [0, 0]) (.const ``String []) (.const ``Bool [])) + let noInternalId : Expr := .app (.const ``Option.none [0]) (.const ``InternalId []) + let strSummarize ← Meta.mkAppM ``Prod.mk #[mkStrLit str.getString, toExpr opts.summarize] + let strSummarizeT ← Meta.inferType strSummarize + -- Can't use mkAppM here because the output severity constant isn't yet defined when this runs + let sevStrSummarize := mkApp4 (.const ``Prod.mk [0, 0]) (.const ``MessageSeverity []) strSummarizeT (.const outputSeverityName.getId []) strSummarize + let inst ← Meta.synthInstance (.app (.const ``ToJson [0]) t) + let which := mkApp3 (.const ``Verso.Genre.Manual.Block.mk []) (toExpr Verso.Genre.Manual.InlineLean.Block.leanOutput.name) noInternalId (mkApp3 (.const ``ToJson.toJson [0]) t inst sevStrSummarize) + let code := mkApp2 (.const ``Block.code []) g (mkStrLit str.getString) + let code ← DocElabM.blockArray #[code] + return mkApp3 (.const ``Block.other []) g which code else - return #[] + return mkApp2 (.const ``Block.concat []) g (← DocElabM.blockArray #[]) open Lean.Parser in -@[code_block_expander tacticStep] -def tacticStep : CodeBlockExpander +@[code_block_elab tacticStep] +def tacticStep : CodeBlockElab | args, str => do let () ← ArgParse.done.run args @@ -435,11 +624,16 @@ def tacticStep : CodeBlockExpander throwErrorAt str "Failed to parse tactic step" | .ok stx => let hlTac ← saveTactic stx - pure #[← ``(Block.other (Verso.Genre.Manual.InlineLean.Block.lean $hlTac) #[Block.code $(quote str.getString)])] + let g ← DocElabM.genreExpr + let which := .app (.const ``Verso.Genre.Manual.InlineLean.Block.lean []) (.const hlTac.getId []) + let code := mkApp2 (.const ``Block.code []) g (mkStrLit str.getString) + let code ← DocElabM.blockArray #[code] + pure <| mkApp3 (.const ``Block.other []) g which code + open Lean.Parser in -@[role_expander tacticStep] -def tacticStepInline : RoleExpander +@[role_elab tacticStep] +def tacticStepInline : RoleElab | args, inlines => do let () ← ArgParse.done.run args let #[arg] := inlines @@ -457,166 +651,10 @@ def tacticStepInline : RoleExpander throwErrorAt arg "Failed to parse tactic step" | .ok stx => let hlTac ← saveTactic stx - - pure #[← ``(Inline.other (Verso.Genre.Manual.InlineLean.Inline.lean $hlTac) #[Inline.code $(quote tacStr.getString)])] - -def Block.proofState : Block where - name := `Manual.proofState - -structure ProofStateOptions where - tag : Option String := none - - -def ProofStateOptions.parse [Monad m] [MonadInfoTree m] [MonadLiftT CoreM m] [MonadEnv m] [MonadError m] : ArgParse m ProofStateOptions := - ProofStateOptions.mk <$> .named `tag .string true - - -open Lean.Parser in -/-- -Show a proof state in the text. The proof goal is expected as a documentation comment immediately -prior to tactics. --/ -@[code_block_expander proofState] -def proofState : CodeBlockExpander - | args, str => do - let opts ← ProofStateOptions.parse.run args - let altStr ← parserInputString str - let p := - node nullKind <| - andthen ⟨{}, whitespace⟩ <| - andthen termParser <| - andthen ⟨{}, whitespace⟩ <| - andthen ":=" <| andthen ⟨{}, whitespace⟩ <| andthen "by" <| - andthen ⟨{}, whitespace⟩ <| - andthen (andthen {fn := (fun _ => (·.pushSyntax (mkIdent `tacticSeq)))} (parserOfStack 0)) <| - optional <| - andthen ⟨{}, whitespace⟩ <| - Command.docComment - match runParser (← getEnv) (← getOptions) p altStr (← getFileName) with - | .error es => - for (pos, msg) in es do - log (severity := .error) (mkErrorStringWithPos "" pos msg) - throwErrorAt str "Failed to parse config (expected goal term, followed by ':=', 'by', and tactics, with optional docstring)" - | .ok stx => - let goalStx := stx[0] - let tacticStx := stx[4] - let desired := - match stx[5][0] with - | .missing => none - | other => some (⟨other⟩ : TSyntax `Lean.Parser.Command.docComment) - let goalExpr ← runWithOpenDecls <| runWithVariables fun _ => Elab.Term.elabTerm goalStx none - let mv ← Meta.mkFreshExprMVar (some goalExpr) - let Expr.mvar mvarId := mv - | throwError "Not an mvar!" - let (remainingGoals, infoTree) ← withInfoTreeContext (mkInfoTree := mkInfoTree `proofState (← getRef)) do - Tactic.run mvarId <| - withoutTacticIncrementality true <| - withTacticInfoContext tacticStx do - evalTactic tacticStx - synthesizeSyntheticMVars (postpone := .no) - let ci : ContextInfo := { - env := ← getEnv, fileMap := ← getFileMap, ngen := ← getNGen, - mctx := ← getMCtx, options := ← getOptions, - currNamespace := ← getCurrNamespace, openDecls := ← getOpenDecls - } - let hlState ← highlightProofState ci remainingGoals (PersistentArray.empty.push infoTree) - let st := goalsToMessageData remainingGoals - --logInfoAt proofPrefix st1 - let stStr ← (← addMessageContext st).toString - if let some s := desired then - if normalizeMetavars stStr.trim != normalizeMetavars s.getDocString.trim then - logErrorAt s m!"Expected: {indentD stStr}\n\nGot: {indentD s.getDocString}" - Verso.Doc.Suggestion.saveSuggestion s (stStr.take 30 ++ "…") ("/--\n" ++ stStr ++ "\n-/\n") - pure #[← `(Doc.Block.other {Block.proofState with data := ToJson.toJson (α := Option String × Array (Highlighted.Goal Highlighted)) ($(quote opts.tag), $(quote hlState))} #[Doc.Block.code $(quote stStr)])] - -where - mkInfoTree (elaborator : Name) (stx : Syntax) (trees : PersistentArray InfoTree) : DocElabM InfoTree := do - let tree := InfoTree.node (Info.ofCommandInfo { elaborator, stx }) trees - let ctx := PartialContextInfo.commandCtx { - env := ← getEnv, fileMap := ← getFileMap, mctx := {}, currNamespace := ← getCurrNamespace, - openDecls := ← getOpenDecls, options := ← getOptions, ngen := ← getNGen - } - return InfoTree.context ctx tree - - modifyInfoTrees {m} [Monad m] [MonadInfoTree m] (f : PersistentArray InfoTree → PersistentArray InfoTree) : m Unit := - modifyInfoState fun s => { s with trees := f s.trees } - - -- TODO - consider how to upstream this - withInfoTreeContext {m α} [Monad m] [MonadInfoTree m] [MonadFinally m] (x : m α) (mkInfoTree : PersistentArray InfoTree → m InfoTree) : m (α × InfoTree) := do - let treesSaved ← getResetInfoTrees - MonadFinally.tryFinally' x fun _ => do - let st ← getInfoState - let tree ← mkInfoTree st.trees - modifyInfoTrees fun _ => treesSaved.push tree - pure tree - - - - -def proofStateStyle := r#" -.hl.lean.tactic-view { - white-space: collapse; -} -.hl.lean.tactic-view .tactic-state { - display: block; - left: 0; - padding: 0; - border: none; -} -.hl.lean.tactic-view .tactic-state .goal { - margin-top: 1em; - margin-bottom: 1em; - display: block; -} -.hl.lean.tactic-view .tactic-state .goal:first-child { - margin-top: 0.25em; -} -.hl.lean.tactic-view .tactic-state .goal:last-child { - margin-bottom: 0.25em; -} - - -"# - - - -@[block_extension Manual.proofState] -def proofState.descr : BlockDescr where - traverse id data content := do - match FromJson.fromJson? data (α := Option String × Array (Highlighted.Goal Highlighted)) with - | .error e => logError s!"Error deserializing proof state info: {e}"; pure none - | .ok (none, _) => pure none - | .ok (some t, v) => - let path ← (·.path) <$> read - let _tag ← Verso.Genre.Manual.externalTag id path t - pure <| some <| Block.other {Block.proofState with id := some id, data := ToJson.toJson (α := (Option String × _)) (none, v)} content - - toTeX := none - extraCss := [highlightingStyle, proofStateStyle] - extraJs := [highlightingJs] - extraJsFiles := [("popper.js", popper), ("tippy.js", tippy)] - extraCssFiles := [("tippy-border.css", tippy.border.css)] - toHtml := - open Verso.Output.Html in - some <| fun _ _ id data _ => do - match FromJson.fromJson? (α := Option Tag × Array (Highlighted.Goal Highlighted)) data with - | .error err => - HtmlT.logError <| "Couldn't deserialize proof state while rendering HTML: " ++ err - pure .empty - | .ok (_, goals) => - let xref ← HtmlT.state - let idAttr := xref.htmlId id - - pure {{ -
-
- {{← if goals.isEmpty then - pure {{"All goals completed! 🐙"}} - else - .seq <$> goals.mapIndexedM (fun ⟨i, _⟩ x => withCollapsedSubgoals .never <| x.toHtml (·.toHtml) i)}} -
-
- }} + let g ← DocElabM.genreExpr + let code := mkApp2 (.const ``Inline.code []) g (mkStrLit tacStr.getString) + let which := .app (.const ``InlineLean.Inline.lean []) (.const hlTac.getId []) + return mkApp3 (.const ``Inline.other []) g which (← DocElabM.inlineArray #[code]) structure StateConfig where tag : Option String := none @@ -625,27 +663,106 @@ structure StateConfig where def StateConfig.parse [Monad m] [MonadInfoTree m] [MonadLiftT CoreM m] [MonadEnv m] [MonadError m] : ArgParse m StateConfig := StateConfig.mk <$> .named `tag .string true <*> ((·.getD true) <$> .named `show .bool true) -@[code_block_expander pre] -def pre : CodeBlockExpander +@[code_block_elab pre] +def pre : CodeBlockElab | args, str => do let opts ← StateConfig.parse.run args let hlPre ← savePre str - -- The quote step here is to prevent the editor from showing document AST internals when the - -- cursor is on the code block + + let g ← DocElabM.genreExpr if opts.show then - pure #[← `(Doc.Block.other {Block.proofState with data := ToJson.toJson (α := Option String × Array (Highlighted.Goal Highlighted)) ($(quote opts.tag), $(hlPre))} #[Doc.Block.code $(quote str.getString)])] + let whichBlock : Expr := mkApp2 (.const ``Block.proofState []) (toExpr opts.tag) (.const hlPre.getId []) + let codeBlock : Expr := mkApp2 (.const ``Doc.Block.code []) g (mkStrLit str.getString) + return mkApp3 (.const ``Doc.Block.other []) g whichBlock (← DocElabM.blockArray #[codeBlock]) else - pure #[] + return mkApp2 (.const ``Block.concat []) g (← DocElabM.blockArray #[]) -@[code_block_expander post] -def post : CodeBlockExpander +@[code_block_elab post] +def post : CodeBlockElab | args, str => do let opts ← StateConfig.parse.run args let hlPost ← savePost str - -- The quote step here is to prevent the editor from showing document AST internals when the - -- cursor is on the code block + + let g ← DocElabM.genreExpr if opts.show then - pure #[← `(Doc.Block.other {Block.proofState with data := ToJson.toJson (α := Option String × Array (Highlighted.Goal Highlighted)) ($(quote opts.tag), $(hlPost))} #[Doc.Block.code $(quote str.getString)])] + let whichBlock : Expr := mkApp2 (.const ``Block.proofState []) (toExpr opts.tag) (.const hlPost.getId []) + let codeBlock : Expr := mkApp2 (.const ``Doc.Block.code []) g (mkStrLit str.getString) + return mkApp3 (.const ``Doc.Block.other []) g whichBlock (← DocElabM.blockArray #[codeBlock]) else - pure #[] + return mkApp2 (.const ``Block.concat []) g (← DocElabM.blockArray #[]) + + +private def specialNames := [``setup, ``goal, ``tacticStep, ``pre, ``post, ``tacticOutput] + +@[directive_elab ref] +private def ref : DirectiveElab + | args, #[] => do + let (x : Ident) ← ArgParse.run (.positional' `name) args + Term.elabTerm x (some (← DocElabM.blockType)) + | _, _ => throwError "Invalid use of `ref`" + +@[role_elab ref] +private def refInline : RoleElab + | args, #[] => do + let (x : Ident) ← ArgParse.run (.positional' `name) args + Term.elabTerm x (some (← DocElabM.inlineType)) + | _, _ => throwError "Invalid use of `ref`" + +private partial def liftSpecialBlocks (stx : Syntax) : StateT (Array (Ident × (TSyntax `inline ⊕ TSyntax `block))) DocElabM Syntax := + stx.replaceM fun s => + match s with + | `(block|```$nameStx:ident $_args*|$_contents:str```) => do + let name ← realizeGlobalConstNoOverload nameStx + if name ∈ specialNames then + let x ← mkFreshUserName <| name.componentsRev.find? (· matches .str _ _) |>.getD `x + let x := mkIdentFrom s x + modify (·.push (x, .inr ⟨s⟩)) + let b' ← `(block|:::ref $x:ident {}) + pure (some b') + else pure none + | `(inline|role{$nameStx $_*}[$_contents*]) => do + let name ← realizeGlobalConstNoOverload nameStx + if name ∈ specialNames then + let x ← mkFreshUserName <| name.componentsRev.find? (· matches .str _ _) |>.getD `x + let x := mkIdentFrom s x + modify (·.push (x, .inl ⟨s⟩)) + let i' ← `(inline|role{ref $x:ident}[]) + pure (some i') + else pure none + | _ => pure none + +@[directive_elab tacticExample] +def tacticExample : DirectiveElab + | args, blocks => do + ArgParse.done.run args + let g ← DocElabM.genreExpr + try + startExample + let (blocks, lifted) ← StateT.run (blocks.mapM (liftSpecialBlocks ·.raw)) #[] + let bt ← DocElabM.blockType + let it ← DocElabM.inlineType + -- First elaborate the special elements, which has a side effect on the environment extension + let lifted ← lifted.mapM fun + | (x, .inr b) => do + let b ← elabBlock' b >>= instantiateMVars + pure (x, bt, b) + | (x, .inl i) => do + let i ← elabInline' i >>= instantiateMVars + pure (x, it, i) + -- Use the extension's data to create helper definitions + endExampleSetup + -- Create definitions for the lifted blocks + for (x, t, e) in lifted do + addAndCompile <| .defnDecl { + name := x.getId, levelParams := [], type := t, value := e, hints := .opaque, safety := .safe + } + -- Block until all helpers are ready before elaborating the final document + for (x, _) in lifted do + if (← getEnv).find? x.getId |>.isSome then continue else break + + let body ← blocks.mapM (elabBlock' ⟨·⟩) + return mkApp2 (.const ``Block.concat []) g (← Meta.mkArrayLit (← DocElabM.blockType) body.toList) + finally + modifyEnv fun env => + tacticExampleCtx.setState env none diff --git a/Manual/NotationsMacros.lean b/Manual/NotationsMacros.lean index d3e378b2..d19b8ed3 100644 --- a/Manual/NotationsMacros.lean +++ b/Manual/NotationsMacros.lean @@ -918,9 +918,9 @@ some 4 :::example "Scoped Macros" Scoped macro rules are active only in their namespace. When the namespace `ConfusingNumbers` is open, numeric literals will be assigned an incorrect meaning. -````lean +```lean namespace ConfusingNumbers -```` +``` The following macro recognizes terms that are odd numeric literals, and replaces them with double their value. If it unconditionally replaced them with double their value, then macro expansion would become an infinite loop because the same rule would always match the output. @@ -934,9 +934,9 @@ scoped macro_rules ``` Once the namespace ends, the macro is no longer used. -````lean +```lean end ConfusingNumbers -```` +``` Without opening the namespace, numeric literals function in the usual way. ```lean (name := nums1) diff --git a/Manual/NotationsMacros/Delab.lean b/Manual/NotationsMacros/Delab.lean index 0fb22f75..ce24be17 100644 --- a/Manual/NotationsMacros/Delab.lean +++ b/Manual/NotationsMacros/Delab.lean @@ -95,7 +95,7 @@ Registers an unexpander of type {name}`Unexpander` for applications of a constan :::::example "Custom Unit Type" -::::keepEnv +:::keepEnv A type equivalent to {lean}`Unit`, but with its own notation, can be defined as a zero-field structure and a macro: ```lean structure Solo where @@ -121,7 +121,7 @@ v : Solo ``` This proof state shows the constructor using {tech}[structure instance] syntax. An unexpander can be used to override this choice. -Because {name}`Solo.mk` cannot be applied to any arguments, the unexpander is free to ignore the syntax, which will always be {lean (type := "UnexpandM Syntax")}``` `(Solo.mk) ```. +Because {name}`Solo.mk` cannot be applied to any arguments, the unexpander is free to ignore the syntax, which will always be {lean (type := "UnexpandM Syntax")}`` `(Solo.mk) ``. ```lean @[app_unexpander Solo.mk] @@ -139,7 +139,7 @@ v : Solo -/ ``` -:::: +::: ::::: :::::example "Unexpansion and Arguments" diff --git a/Manual/RecursiveDefs/WF.lean b/Manual/RecursiveDefs/WF.lean index 0e7ab0c8..f3626b53 100644 --- a/Manual/RecursiveDefs/WF.lean +++ b/Manual/RecursiveDefs/WF.lean @@ -73,7 +73,7 @@ tag := "wf-rel" A relation `≺` is a {deftech}_well-founded relation_ if there exists no infinitely descending chain -$$`` x_0 ≻ x_1 ≻ \cdots`` +$$` x_0 ≻ x_1 ≻ \cdots` In Lean, types that are equipped with a canonical well-founded relation are instances of the {name}`WellFoundedRelation` type class. diff --git a/Manual/RecursiveDefs/WF/PreprocessExample.lean b/Manual/RecursiveDefs/WF/PreprocessExample.lean index 5969a305..0deac9c8 100644 --- a/Manual/RecursiveDefs/WF/PreprocessExample.lean +++ b/Manual/RecursiveDefs/WF/PreprocessExample.lean @@ -176,7 +176,9 @@ macro "sizeOf_pair_dec" : tactic => omega done) -macro_rules | `(tactic| decreasing_trivial) => `(tactic| sizeOf_pair_dec) +macro_rules + | `(tactic| decreasing_trivial) => + `(tactic| sizeOf_pair_dec) def Tree.map (f : α → β) : Tree α → Tree β | leaf x => leaf (f x) diff --git a/Manual/Simp.lean b/Manual/Simp.lean index 538de076..c3b02657 100644 --- a/Manual/Simp.lean +++ b/Manual/Simp.lean @@ -433,10 +433,12 @@ Try this: simp only [List.size_toArray, List.length_cons, List.length_nil, Nat.z ``` which results in the more maintainable proof: ```lean -example (xs : Array Unit) : xs.size = 2 → xs = #[(), ()] := by +example (xs : Array Unit) : + xs.size = 2 → xs = #[(), ()] := by intros ext - simp only [List.size_toArray, List.length_cons, List.length_nil, Nat.zero_add, Nat.reduceAdd] + simp only [List.size_toArray, List.length_cons, + List.length_nil, Nat.zero_add, Nat.reduceAdd] assumption ``` diff --git a/Manual/Tactics/Reference.lean b/Manual/Tactics/Reference.lean index 32caa73d..f20af696 100644 --- a/Manual/Tactics/Reference.lean +++ b/Manual/Tactics/Reference.lean @@ -491,8 +491,8 @@ Try this: exact Nat.lt_trans h1 h2 ``` ```post (show := false) - ``` + ::: diff --git a/Manual/Terms.lean b/Manual/Terms.lean index b0cf7739..f35e71f0 100644 --- a/Manual/Terms.lean +++ b/Manual/Terms.lean @@ -85,7 +85,6 @@ If an identifier resolves to multiple names, then the elaborator attempts to use If exactly one of them succeeds, then it is used as the meaning of the identifier. It is an error if more than one succeed or if all fail. -::::keepEnv :::example "Local Names Take Precedence" Local bindings take precedence over global bindings: ```lean (name := localOverGlobal) @@ -109,9 +108,8 @@ The innermost local binding of a name takes precedence over others: "inner" ``` ::: -:::: -::::keepEnv + :::example "Longer Prefixes of Current Namespace Take Precedence" The namespaces `A`, `B`, and `C` are nested, and `A` and `C` each contain a definition of `x`. ```lean (name := NS) @@ -138,9 +136,8 @@ end C "A.x" ``` ::: -:::: -::::keepEnv + :::example "Longer Identifier Prefixes Take Precedence" When an identifier could refer to different projections from names, the one with the longest name takes precedence: ```lean @@ -164,9 +161,8 @@ It refers to the {name A.y}`y` field of {name}`y.y`, because the name {name}`y.y "longer" ``` ::: -:::: -::::keepEnv + :::example "Current Namespace Contents Take Precedence Over Opened Namespaces" When an identifier could refer either to a name defined in a prefix of the current namespace or to an opened namespace, the former takes precedence. ```lean @@ -188,7 +184,6 @@ Even though `A` was opened more recently than the declaration of {name}`B.x`, th "B.x" ``` ::: -:::: :::example "Ambiguous Identifiers" @@ -716,9 +711,9 @@ When a function is found, the term before the dot becomes an argument to the fun Specifically, it becomes the first explicit argument that would not be a type error. Aside from that, the application is elaborated as usual. -::::keepEnv + +::::leanSection ```lean (show := false) -section variable (name : Username) ``` :::example "Generalized Field Notation" @@ -767,9 +762,7 @@ has type Except.ok () ``` ::: -```lean (show := false) -end -``` + :::: {optionDocs pp.fieldNotation} @@ -1429,11 +1422,10 @@ To support dependent types, matching a discriminant against a pattern refines th In both subsequent patterns in the same match alternative and the right-hand side's type, occurrences of the discriminant are replaced by the pattern that it was matched against. -::::keepEnv +::::leanSection ```lean (show := false) variable {α : Type u} ``` - :::example "Type Refinement" This {tech}[indexed family] describes mostly-balanced trees, with the depth encoded in the type. ```lean @@ -1487,7 +1479,7 @@ depth n : Nat Matching on the depth of a tree and the tree itself leads to a refinement of the tree's type according to the depth's pattern. This means that certain combinations are not well-typed, such as {lean}`0` and {name BalancedTree.branch}`branch`, because refining the second discriminant's type yields {lean}`BalancedTree α 0` which does not match the constructor's type. -````lean (name := patfail) (error := true) +```lean (name := patfail) (error := true) def BalancedTree.isPerfectlyBalanced (n : Nat) (t : BalancedTree α n) : Bool := match n, t with @@ -1496,7 +1488,7 @@ def BalancedTree.isPerfectlyBalanced isPerfectlyBalanced left && isPerfectlyBalanced right | _, _ => false -```` +``` ```leanOutput patfail type mismatch left.branch val right @@ -1508,6 +1500,7 @@ but is expected to have type ::: :::: + ### Pattern Equality Proofs When a discriminant is named, {keywordOf Lean.Parser.Term.match}`match` generates a proof that the pattern and discriminant are equal, binding it to the provided name in the {tech}[right-hand side]. @@ -1674,9 +1667,8 @@ match_pattern ``` ::: -::::keepEnv +::::leanSection ```lean (show := false) -section variable {k : Nat} ``` :::example "Match Patterns Follow Reduction" @@ -1706,13 +1698,10 @@ No {tech}[ι-reduction] is possible, because the value being matched is a variab In the case of {lean}`k + 1`, that is, {lean}`Nat.add k (.succ .zero)`, the second pattern matches, so it reduces to {lean}`Nat.succ (Nat.add k .zero)`. The second pattern now matches, yielding {lean}`Nat.succ k`, which is a valid pattern. ::: -````lean (show := false) -end -```` - :::: + ```lean (show := false) end ``` diff --git a/Manual/Types.lean b/Manual/Types.lean index a359f218..b78a2afe 100644 --- a/Manual/Types.lean +++ b/Manual/Types.lean @@ -104,12 +104,12 @@ def LengthList (α : Type u) : Nat → Type u ``` Because Lean's tuples nest to the right, multiple nested parentheses are not needed: -````lean +```lean example : LengthList Int 0 := () example : LengthList String 2 := ("Hello", "there", ()) -```` +``` If the length does not match the number of entries, then the computed type will not match the term: ```lean error:=true name:=wrongNum @@ -398,18 +398,18 @@ tag := "level-expressions" Levels that occur in a definition are not restricted to just variables and addition of constants. More complex relationships between universes can be defined using level expressions. -```` +``` Level ::= 0 | 1 | 2 | ... -- Concrete levels | u, v -- Variables | Level + n -- Addition of constants | max Level Level -- Least upper bound | imax Level Level -- Impredicative LUB -```` +``` Given an assignment of level variables to concrete numbers, evaluating these expressions follows the usual rules of arithmetic. The `imax` operation is defined as follows: -$$``\mathtt{imax}\ u\ v = \begin{cases}0 & \mathrm{when\ }v = 0\\\mathtt{max}\ u\ v&\mathrm{otherwise}\end{cases}`` +$$`\mathtt{imax}\ u\ v = \begin{cases}0 & \mathrm{when\ }v = 0\\\mathtt{max}\ u\ v&\mathrm{otherwise}\end{cases}` `imax` is used to implement {tech}[impredicative] quantification for {lean}`Prop`. In particular, if `A : Sort u` and `B : Sort v`, then `(x : A) → B : Sort (imax u v)`. diff --git a/lake-manifest.json b/lake-manifest.json index af68126f..eb50bea4 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -5,10 +5,10 @@ "type": "git", "subDir": null, "scope": "", - "rev": "6d3c402b46e9ccac560c0e8eac725005588391fb", + "rev": "a336a39348976abbfd10e156c56707ce01a3bb9d", "name": "verso", "manifestFile": "lake-manifest.json", - "inputRev": "main", + "inputRev": "more-elab", "inherited": false, "configFile": "lakefile.lean"}, {"url": "https://github.com/acmepjz/md4lean", diff --git a/lakefile.lean b/lakefile.lean index 9ffd1af5..e8c48000 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -8,7 +8,7 @@ open Lake DSL open System (FilePath) require MD4Lean from git "https://github.com/acmepjz/md4lean"@"main" -require verso from git "https://github.com/leanprover/verso.git"@"main" +require verso from git "https://github.com/leanprover/verso.git"@"more-elab" package "verso-manual" where -- building the C code cost much more than the optimizations save