cleanup + ci

.github/workflows/ci.yml

@@ -93,6 +93,7 @@ jobs:
             sourcesanspro
             sourceserifpro
             fvextra
+            upquote
 
       - name: Check `tlmgr` version
         run: tlmgr --version

doc/UsersGuide/Basic.lean

@@ -67,6 +67,14 @@ results in
 
 {docstring Monad}
 
+:::tactic "induction"
+:::
+
+:::tactic "simp"
+:::
+
+
+
 # Index
 %%%
 number := false

src/verso-manual/VersoManual/Docstring.lean

@@ -71,7 +71,7 @@ def ppName (c : Name) (showUniverses := true) (showNamespace : Bool := true) (op
 
 open Lean.PrettyPrinter Delaborator in
 def ppSignature (c : Name) (showNamespace : Bool := true) (openDecls : List OpenDecl := []) : MetaM FormatWithInfos :=
-  MonadWithReaderOf.withReader (fun (ρ : Core.Context) => {ρ with openDecls := ρ.openDecls ++ openDecls}) <|do
+  withTheReader Core.Context (fun ρ => {ρ with openDecls := ρ.openDecls ++ openDecls}) <| do
   let decl ← getConstInfo c
   let e := .const c (decl.levelParams.map mkLevelParam)
   let (stx, infos) ← delabCore e (delab := delabConstWithSignature)
@@ -227,8 +227,6 @@ def DeclType.label : DeclType → String
   | .inductive _ _ true => "inductive predicate"
   | other => ""
 
-set_option pp.fullNames false in
-#check List.nil
 
 open Meta in
 def DocName.ofName (c : Name) (ppWidth : Nat := 40) (showUniverses := true) (showNamespace := true) (openDecls : List OpenDecl := []) : MetaM DocName := do
@@ -246,6 +244,7 @@ def DocName.ofName (c : Name) (ppWidth : Nat := 40) (showUniverses := true) (sho
 
     let ⟨fmt, infos⟩ ← withOptions (·.setBool `pp.tagAppFns true) <|
       ppSignature c (showNamespace := showNamespace) (openDecls := openDecls)
+
     let ttSig := Lean.Widget.TaggedText.prettyTagged (w := ppWidth) fmt
     let sig := Lean.Widget.tagCodeInfos ctx infos ttSig
 
@@ -808,21 +807,17 @@ def tryElabInlineCodeTerm (str : String) : DocElabM Term := do
   match Parser.runParserCategory (← getEnv) `term str src with
   | .error e => throw (.error (← getRef) e)
   | .ok stx =>
-    dbg_trace "PARSED |{stx}|"
     let (newMsgs, tree, e) ← do
       let initMsgs ← Core.getMessageLog
       try
         Core.resetMessageLog
         -- TODO open decls/current namespace
         let (tree', e') ← fun _ => do
-          dbg_trace "Gonna elab..."
           let e ← Elab.Term.elabTerm (catchExPostpone := true) stx none
-          dbg_trace "ELAB'ED! |{e}|"
           Term.synthesizeSyntheticMVarsNoPostponing
           let e' ← Term.levelMVarToParam (← instantiateMVars e)
           Term.synthesizeSyntheticMVarsNoPostponing
           let e' ← instantiateMVars e'
-          dbg_trace "ELAB'ED MORE! |{e'}|"
           let ctx := PartialContextInfo.commandCtx {
             env := ← getEnv, fileMap := ← getFileMap, mctx := ← getMCtx, currNamespace := ← getCurrNamespace,
             openDecls := ← getOpenDecls, options := ← getOptions, ngen := ← getNGen