Cites

Manual/Language/RecursiveDefs/WF.lean

@@ -7,6 +7,7 @@ Author: Joachim Breitner
 import VersoManual
 
 import Manual.Meta
+import Manual.Papers
 import Manual.Language.RecursiveDefs.WF.GuessLexExample
 
 open Manual
@@ -511,8 +512,7 @@ To infer a suitable termination {tech}[measure], Lean considers multiple {deftec
 The basic termination measures considered are:
 
 * all parameters whose type have a non-trivial {name}`SizeOf` instance
-* the expression `e₂ - e₁` whenever the local context of a recursive call has an assumption of type `e₁ < e₂` or `e₁ ≤ e₂`, where `e₁` and `e₂` are of type {name}`Nat` and depend only on the function's parameters. {TODO}[Cite “Termination Analysis with Calling Context Graphs” by Panagiotis Manolios &
-Daron Vroon, `https://doi.org/10.1007/11817963_36`.]
+* the expression `e₂ - e₁` whenever the local context of a recursive call has an assumption of type `e₁ < e₂` or `e₁ ≤ e₂`, where `e₁` and `e₂` are of type {name}`Nat` and depend only on the function's parameters. {margin}[This approach is based on work by {citehere manolios2006}[].]
 * in a {tech}[mutual group], an additional basic measure is used to distinguish between recursive calls to other functions in the group and recursive calls to the function being defined (for details, see {ref "mutual-well-founded-recursion"}[the section on mutual well-founded recursion])
 
 {deftech}_Candidate measures_ are basic measures or tuples of basic measures.
@@ -524,10 +524,8 @@ It can be automatically added to the source file using the offered suggestion or
 To avoid the combinatorial explosion of trying all tuples of measures, Lean first tabulates all {tech}[basic termination measures], determining whether the basic measure is decreasing, strictly decreasing, or non-decreasing.
 A decreasing measure is smaller for at least one recursive call and never increases at any recursive call, while a strictly decreasing measure is smaller at all recursive calls.
 A non-decreasing measure is one that the termination tactic could not show to be decreasing or strictly decreasing.
-A suitable tuple is chosen based on the table.
+A suitable tuple is chosen based on the table.{margin}[This approach is based on {citehere bulwahn2007}[].]
 This table shows up in the error message when no automatic measure could be found.
-{TODO}[Cite  “Finding Lexicographic Orders for Termination Proofs in Isabelle/HOL”
-by Lukas Bulwahn, Alexander Krauss, and Tobias Nipkow, `10.1007/978-3-540-74591-4_5`, `https://www21.in.tum.de/~nipkow/pubs/tphols07.pdf`].
 
 {spliceContents Manual.Language.RecursiveDefs.WF.GuessLexExample}
 

Manual/Meta/Example.lean

@@ -113,7 +113,12 @@ r#".example {
   border-radius: 0.5em;
   margin-bottom: 0.75em;
   margin-top: 0.75em;
-  clear: both; /* Don't overlap margin notes with examples */
+}
+/* 1400 px is the cutoff for when the margin notes move out of the margin and into floated elements. */
+@media screen and (700px < width <= 1400px) {
+  .example {
+    clear: both; /* Don't overlap margin notes with examples */
+  }
 }
 .example p:last-child {margin-bottom:0;}
 .example .description::before {

Manual/Papers.lean

@@ -54,3 +54,19 @@ def launchbury94 : InProceedings where
   authors := #[.concat (inlines! "John Launchbury"), .concat (inlines!"Simon L Peyton Jones")]
   year := 1994
   booktitle := .concat (inlines!"Proceedings of the ACM SIGPLAN 1994 Conference on Programming Language Design and Implementation")
+
+def manolios2006 : InProceedings where
+  title := .concat (inlines!"Termination Analysis with Calling Context Graphs")
+  authors := #[.concat (inlines!"Panagiotis Manolios"), .concat (inlines!"Daron Vroon")]
+  year := 2006
+  booktitle := .concat (inlines!"Proceedings of the International Conference on Computer Aided Verification (CAV 2006)")
+  series := some <| .concat (inlines!"LNCS 4144")
+  url := "https://doi.org/10.1007/11817963_36"
+
+def bulwahn2007 : InProceedings where
+  title := .concat (inlines!"Finding Lexicographic Orders for Termination Proofs in Isabelle/HOL")
+  authors := #[.concat (inlines!"Lukas Bulwahn"), .concat (inlines!"Alexander Krauss"), .concat (inlines!"Tobias Nipkow")]
+  year := 2007
+  booktitle := .concat (inlines!"Proceedings of the International Conference on Theorem Proving in Higher Order Logics (TPHOLS 2007)")
+  series := some <| .concat (inlines!"LNTCS 4732")
+  url := "https://doi.org/10.1007/978-3-540-74591-4_5"