feat: well-founded function definition preprocessing (#296)

This documents the changes from leanprover/lean4#6744. --------- Co-authored-by: David Thrane Christiansen <[email protected]>
leanprover · Feb 14, 2025 · 08dd6d1 · 08dd6d1
1 parent 9749cb2
commit 08dd6d1
Show file tree

Hide file tree

Showing 10 changed files with 423 additions and 136 deletions.
diff --git a/.vale/styles/config/ignore/terms.txt b/.vale/styles/config/ignore/terms.txt
@@ -170,3 +170,4 @@ unparenthesized
 uploader
 upvote
 walkthrough
+preprocesses
diff --git a/Manual/BasicTypes.lean b/Manual/BasicTypes.lean
@@ -357,6 +357,9 @@ end ShortCircuit
 {include 0 Manual.BasicTypes.Array}
 
 # Subtypes
+%%%
+tag := "Subtype"
+%%%
 
 :::planned 173
  * When to use them?

diff --git a/Manual/Meta/Lean.lean b/Manual/Meta/Lean.lean
@@ -579,6 +579,8 @@ def signature : CodeBlockExpander
   | args, str => do
     let {«show»} ← SignatureConfig.parse.run args
     let altStr ← parserInputString str
+    let col? := (← getRef).getPos? |>.map (← getFileMap).utf8PosToLspPos |>.map (·.character)
+
 
     match Parser.runParserCategory (← getEnv) `signature_spec altStr (← getFileName) with
     | .error e => throwError e
@@ -602,14 +604,19 @@ def signature : CodeBlockExpander
         try
           let ((hls, _, _, _), st') ← ((SubVerso.Examples.checkSignature name sig).run cmdCtx).run cmdState
           setInfoState st'.infoState
-          pure hls
+          pure (Highlighted.seq hls)
         catch e =>
           let fmt ← PrettyPrinter.ppSignature (TSyntax.mk name.raw[0]).getId
           Suggestion.saveSuggestion str (fmt.fmt.pretty 60) (fmt.fmt.pretty 30 ++ "\n")
           throw e
 
+      let hls :=
+        if let some col := col? then
+          hls.deIndent col
+        else hls
+
       if «show» then
-        pure #[← `(Block.other {Block.signature with data := ToJson.toJson $(quote (Highlighted.seq hls))} #[Block.code $(quote str.getString)])]
+        pure #[← `(Block.other {Block.signature with data := ToJson.toJson $(quote hls)} #[Block.code $(quote str.getString)])]
       else
         pure #[]
 

diff --git a/Manual/Meta/Tactics.lean b/Manual/Meta/Tactics.lean
@@ -563,11 +563,19 @@ def proofStateStyle := r#"
   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;
 }
+
+
 "#