chore: adapt to updated argument and flag syntax

CONTRIBUTING.md

@@ -73,7 +73,7 @@ In addition to what Verso provides, there are a number of additional roles, code
 Please use the following roles where they make sense:
 
  * `` {lean}`TERM` `` - `TERM` is a Lean term, to be elaborated as such and included it in the rendered document with appropriate highlighting.
-   The optional named argument `type` specifies an expected type, e.g. `` {lean type:="Nat"}`.succ .zero` ``
+   The optional named argument `type` specifies an expected type, e.g. `` {lean  (type := "Nat")}`.succ .zero` ``
 
  * `` {name}`X` `` - `X` is a constant in the Lean environment.
    The optional positional argument can be used to override name resolution; if it is provided, then the positional argument is used to resolve the name but the contents of the directive are rendered.

Manual.lean

@@ -111,7 +111,7 @@ draft := true
 
 {docstring Dynamic}
 
-{docstring Dynamic.mk (allowMissing := true)}
+{docstring Dynamic.mk +allowMissing}
 
 {docstring Dynamic.get?}
 

Manual/Attributes.lean

@@ -59,7 +59,7 @@ Each attribute determines how to store its own metadata and what the appropriate
 Attributes can be added to declarations as a {ref "declaration-modifiers"}[declaration modifier].
 They are placed between the documentation comment and the visibility modifiers.
 
-:::syntax Lean.Parser.Term.attributes (open := false) (title := "Attributes")
+:::syntax Lean.Parser.Term.attributes -open (title := "Attributes")
 ```grammar
 @[$_:attrInstance,*]
 ```
@@ -104,7 +104,7 @@ This determines whether the attribute's effect is visible only in the current se
 These scope indications are also used to control {ref "syntax-rules"}[syntax extensions] and {ref "instance-attribute"}[type class instances].
 Each attribute is responsible for defining precisely what these terms mean for its particular effect.
 
-:::syntax attrKind (open := false) (title := "Attribute Scopes") (alias := Lean.Parser.Term.attrKind)
+:::syntax attrKind -open (title := "Attribute Scopes") (alias := Lean.Parser.Term.attrKind)
 Globally-scoped declarations (the default) are in effect whenever the {tech}[module] in which they're established is transitively imported.
 They are indicated by the absence of another scope modifier.
 ```grammar
@@ -115,7 +115,7 @@ Locally-scoped declarations are in effect only for the extent of the {tech}[sect
 local
 ```
 
-Scoped declarations are in effect whenever the {tech key:="current namespace"}[namespace] in which they are established is opened.
+Scoped declarations are in effect whenever the {tech (key := "current namespace")}[namespace] in which they are established is opened.
 ```grammar
 scoped
 ```

Manual/Axioms.lean

@@ -19,13 +19,13 @@ htmlSplit := .never
 %%%
 :::leanSection
 
-```lean (show := false)
+```lean -show
 universe u
 ```
 
 {deftech}_Axioms_ are postulated constants.
 While the axiom's type must itself be a type (that is, it must have type {lean}`Sort u`), there are no further requirements.
-Axioms do not {tech key:="reduction"}[reduce] to other terms.
+Axioms do not {tech (key := "reduction")}[reduce] to other terms.
 :::
 
 Axioms can be used to experiment with the consequences of an idea before investing the time required to construct a model or prove a theorem.
@@ -138,7 +138,7 @@ Definitions that contain non-proof code that relies on axioms must be marked {ke
 :::example "Axioms and Compilation"
 Adding an additional `0` to {lean}`Nat` with an axiom makes it so functions that use it can't be compiled.
 In particular, {name}`List.length'` returns the axiom {name}`Nat.otherZero` instead of {name}`Nat.zero` as the length of the empty list.
-```lean (name := otherZero2) (error := true)
+```lean (name := otherZero2) +error
 axiom Nat.otherZero : Nat
 
 def List.length' : List α → Nat
@@ -224,9 +224,9 @@ However, they allow the use of compiled code in proofs to be carefully controlle
    ```
 
 :::keepEnv
-```lean (show := false)
+```lean -show
 axiom Anything : Type
 ```
-Finally, the axiom {name}`sorryAx` is used as part of the implementation of the {tactic}`sorry` tactic and {lean type:="Anything"}`sorry` term.
+Finally, the axiom {name}`sorryAx` is used as part of the implementation of the {tactic}`sorry` tactic and {lean  (type := "Anything")}`sorry` term.
 Uses of this axiom are not intended to occur in finished proofs, and this can be confirmed using {keywordOf Lean.Parser.Command.printAxioms}`#print axioms`.
 :::

Manual/BasicProps.lean

@@ -99,7 +99,7 @@ However, it should not be confused with {name}`PProd`: using non-computable reas
 
 In a {ref "tactics"}[tactic] proof, conjunctions can be proved using {name}`And.intro` explicitly via {tactic}`apply`, but {tactic}`constructor` is more common.
 When multiple conjunctions are nested in a proof goal, {tactic}`and_intros` can be used to apply {name}`And.intro` in each relevant location.
-Assumptions of conjunctions in the context can be simplified using {tactic}`cases`, pattern matching with {tactic}`let` or {tactic show:="match"}`Lean.Parser.Tactic.match`, or {tactic}`rcases`.
+Assumptions of conjunctions in the context can be simplified using {tactic}`cases`, pattern matching with {tactic}`let` or {tactic (show := "match")}`Lean.Parser.Tactic.match`, or {tactic}`rcases`.
 
 {docstring And}
 
@@ -113,7 +113,7 @@ Because {lean}`Sum` is a type, it is possible to check _which_ constructor was u
 In other words, because {lean}`Or` is not a {tech}[subsingleton], its proofs cannot be used as part of a computation.
 
 In a {ref "tactics"}[tactic] proof, disjunctions can be proved using either constructor ({name}`Or.inl` or {name}`Or.inr`) explicitly via {tactic}`apply`.
-Assumptions of disjunctions in the context can be simplified using {tactic}`cases`, pattern matching with {tactic show:="match"}`Lean.Parser.Tactic.match`, or {tactic}`rcases`.
+Assumptions of disjunctions in the context can be simplified using {tactic}`cases`, pattern matching with {tactic (show := "match")}`Lean.Parser.Tactic.match`, or {tactic}`rcases`.
 
 {docstring Or}
 
@@ -125,14 +125,14 @@ This is because the decision procedure's result provides a suitable branch condi
 {docstring Or.by_cases'}
 
 
-```lean (show := false)
+```lean -show
 section
 variable {P : Prop}
 ```
 Rather than encoding negation as an inductive type, {lean}`¬P` is defined to mean {lean}`P → False`.
 In other words, to prove a negation, it suffices to assume the negated statement and derive a contradiction.
 This also means that {lean}`False` can be derived immediately from a proof of a proposition and its negation, and then used to prove any proposition or inhabit any type.
-```lean (show := false)
+```lean -show
 end
 ```
 
@@ -146,7 +146,7 @@ end
 
 
 
-```lean (show := false)
+```lean -show
 section
 variable {A B : Prop}
 ```
@@ -171,7 +171,7 @@ theorem truth_functional_imp {A B : Prop} :
 ```
 :::
 
-```lean (show := false)
+```lean -show
 end
 ```
 
@@ -239,7 +239,7 @@ Unlike both {name}`Subtype` and {name}`Sigma`, it is a {tech}[proposition]; this
 
 When writing a proof, the {tactic}`exists` tactic allows one (or more) witness(es) to be specified for a (potentially nested) existential statement.
 The {tactic}`constructor` tactic, on the other hand, creates a {tech}[metavariable] for the witness; providing a proof of the predicate may solve the metavariable as well.
-The components of an existential assumption can be made available individually by pattern matching with {tactic}`let` or {tactic show:="match"}`Lean.Parser.Tactic.match`, as well as by using {tactic}`cases` or {tactic}`rcases`.
+The components of an existential assumption can be made available individually by pattern matching with {tactic}`let` or {tactic (show := "match")}`Lean.Parser.Tactic.match`, as well as by using {tactic}`cases` or {tactic}`rcases`.
 
 :::example "Proving Existential Statements"
 
@@ -402,12 +402,12 @@ In these cases, the built-in automation has no choice but to use heterogeneous e
 $_ ≍ $_
 ```
 
-```lean (show := false)
+```lean -show
 section
 variable (x : α) (y : β)
 ```
 Heterogeneous equality {lean}`HEq x y` can be written {lean}`x ≍ y`.
-```lean (show := false)
+```lean -show
 end
 ```
 
@@ -418,7 +418,7 @@ end
 
 :::::leanSection
 ::::example "Heterogeneous Equality"
-```lean (show := false)
+```lean -show
 variable {α : Type u} {n k l₁ l₂ l₃ : Nat}
 ```
 
@@ -429,7 +429,7 @@ variable
   {xs : Vector α l₁} {ys : Vector α l₂} {zs : Vector α l₃}
 set_option linter.unusedVariables false
 ```
-```lean (name := assocFail) (error := true) (keep := false)
+```lean (name := assocFail) +error -keep
 theorem Vector.append_associative :
     xs ++ (ys ++ zs) = (xs ++ ys) ++ zs := by sorry
 ```
@@ -456,15 +456,15 @@ However, such proof statements can be difficult to work with in certain circumst
 
 :::paragraph
 Another is to use heterogeneous equality:
-```lean (keep := false)
+```lean -keep
 theorem Vector.append_associative :
     HEq (xs ++ (ys ++ zs)) ((xs ++ ys) ++ zs) := by sorry
 ```
 :::
 
 In this case, {ref "the-simplifier"}[the simplifier] can rewrite both sides of the equation without having to preserve their types.
 However, proving the theorem does require eventually proving that the lengths nonetheless match.
-```lean (keep := false)
+```lean -keep
 theorem Vector.append_associative :
     HEq (xs ++ (ys ++ zs)) ((xs ++ ys) ++ zs) := by
   cases xs; cases ys; cases zs

Manual/BasicTypes.lean

@@ -69,7 +69,7 @@ In functional programming, {lean}`Unit` is the return type of things that "retur
 Mathematically, this is represented by a single completely uninformative value, as opposed to an empty type such as {lean}`Empty`, which represents unreachable code.
 
 :::leanSection
-```lean (show := false)
+```lean -show
 variable {m : Type → Type} [Monad m] {α : Type}
 ```
 
@@ -85,7 +85,7 @@ There are two variants of the unit type:
 
  * {lean}`Unit` is a {lean}`Type` that exists in the smallest non-propositional {tech}[universe].
 
- * {lean}`PUnit` is {tech key:="universe polymorphism"}[universe polymorphic] and can be used in any non-propositional {tech}[universe].
+ * {lean}`PUnit` is {tech (key := "universe polymorphism")}[universe polymorphic] and can be used in any non-propositional {tech}[universe].
 
 Behind the scenes, {lean}`Unit` is actually defined as {lean}`PUnit.{1}`.
 {lean}`Unit` should be preferred over {name}`PUnit` when possible to avoid unnecessary universe parameters.
@@ -101,7 +101,7 @@ If in doubt, use {lean}`Unit` until universe errors occur.
 
 {deftech}_Unit-like types_ are inductive types that have a single constructor which takes no non-proof parameters.
 {lean}`PUnit` is one such type.
-All elements of unit-like types are {tech key:="definitional equality"}[definitionally equal] to all other elements.
+All elements of unit-like types are {tech (key := "definitional equality")}[definitionally equal] to all other elements.
 
 :::example "Definitional Equality of {lean}`Unit`"
 Every term with type {lean}`Unit` is definitionally equal to every other term with type {lean}`Unit`:
@@ -143,7 +143,7 @@ inductive NotUnitLike where
   | mk (u : Unit)
 ```
 
-```lean (error:=true) (name := NotUnitLike)
+```lean +error (name := NotUnitLike)
 example (e1 e2 : NotUnitLike) : e1 = e2 := rfl
 ```
 ```leanOutput NotUnitLike
@@ -186,7 +186,7 @@ However, there is an important pragmatic difference: {lean}`Bool` classifies _va
 In other words, {lean}`Bool` is the notion of truth and falsehood that's appropriate for programs, while {lean}`Prop` is the notion that's appropriate for mathematics.
 Because proofs are erased from compiled programs, keeping {lean}`Bool` and {lean}`Prop` distinct makes it clear which parts of a Lean file are intended for computation.
 
-```lean (show := false)
+```lean -show
 section BoolProp
 
 axiom b : Bool
@@ -211,7 +211,7 @@ These propositions are called {tech}_decidable_ propositions, and have instances
 The function {name}`Decidable.decide` converts a proof-carrying {lean}`Decidable` result into a {lean}`Bool`.
 This function is also a coercion from decidable propositions to {lean}`Bool`, so {lean}`(2 = 2 : Bool)` evaluates to {lean}`true`.
 
-```lean (show := false)
+```lean -show
 /-- info: true -/
 #check_msgs in
 #eval (2 = 2 : Bool)
@@ -246,7 +246,7 @@ The prefix operator `!` is notation for {lean}`Bool.not`.
 
 ### Logical Operations
 
-```lean (show := false)
+```lean -show
 section ShortCircuit
 
 axiom BIG_EXPENSIVE_COMPUTATION : Bool
@@ -256,7 +256,7 @@ The functions {name}`cond`, {name Bool.and}`and`, and {name Bool.or}`or` are sho
 In other words, {lean}`false && BIG_EXPENSIVE_COMPUTATION` does not need to execute {lean}`BIG_EXPENSIVE_COMPUTATION` before returning `false`.
 These functions are defined using the {attr}`macro_inline` attribute, which causes the compiler to replace calls to them with their definitions while generating code, and the definitions use nested pattern matching to achieve the short-circuiting behavior.
 
-```lean (show := false)
+```lean -show
 end ShortCircuit
 ```
 

Manual/BasicTypes/Array/FFI.lean

@@ -20,7 +20,7 @@ set_option pp.rawOnError true
 tag := "array-ffi"
 %%%
 
-:::ffi "lean_string_object" kind := type
+:::ffi "lean_string_object" (kind := type)
 ```
 typedef struct {
     lean_object   m_header;

Manual/BasicTypes/BitVec.lean

@@ -40,7 +40,7 @@ Because {name}`BitVec` is a {ref "inductive-types-trivial-wrappers"}[trivial wra
 
 # Syntax
 :::leanSection
-```lean (show := false)
+```lean -show
 variable {w n : Nat}
 ```
 There is an {inst}`OfNat (BitVec w) n` instance for all widths {lean}`w` and natural numbers {lean}`n`.
@@ -55,7 +55,7 @@ example : BitVec 8 := 0xff
 example : BitVec 8 := 255
 example : BitVec 8 := 0b1111_1111
 ```
-```lean (show := false)
+```lean -show
 -- Inline test
 example : (0xff : BitVec 8) = 255 := by rfl
 example : (0b1111_1111 : BitVec 8) = 255 := by rfl
@@ -147,7 +147,7 @@ example : BitVec 8 := 1#'(by decide)
 ```
 
 Literals that are not in bounds are not allowed:
-```lean (error := true) (name := oob)
+```lean +error (name := oob)
 example : BitVec 8 := 256#'(by decide)
 ```
 ```leanOutput oob

Manual/BasicTypes/Fin.lean

@@ -18,7 +18,7 @@ open Verso.Genre.Manual.InlineLean
 tag := "Fin"
 %%%
 
-```lean (show := false)
+```lean -show
 section
 variable (n : Nat)
 ```
@@ -92,7 +92,7 @@ When the literal is greater than or equal to {lean}`n`, the remainder when divid
 ```
 
 If Lean can't synthesize an instance of {lean}`NeZero n`, then there is no {lean}`OfNat (Fin n)` instance:
-```lean (error := true) (name := fin0)
+```lean +error (name := fin0)
 example : Fin 0 := 0
 ```
 ```leanOutput fin0
@@ -105,7 +105,7 @@ due to the absence of the instance above
 Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.
 ```
 
-```lean (error := true) (name := finK)
+```lean +error (name := finK)
 example (k : Nat) : Fin k := 0
 ```
 ```leanOutput finK

Manual/BasicTypes/Float.lean

@@ -38,19 +38,19 @@ Lean provides two floating-point types: {name}`Float` represents 64-bit floating
 The precision of {name}`Float` does not vary based on the platform that Lean is running on.
 
 
-{docstring Float (label := "type") (hideStructureConstructor := true) (hideFields := true)}
+{docstring Float (label := "type") +hideStructureConstructor +hideFields}
 
-{docstring Float32 (label := "type") (hideStructureConstructor := true) (hideFields := true)}
+{docstring Float32 (label := "type") +hideStructureConstructor +hideFields}
 
 
 :::example "No Kernel Reasoning About Floating-Point Numbers"
-The Lean kernel can compare expressions of type {lean}`Float` for syntactic equality, so {lean type:="Float"}`0.0` is definitionally equal to itself.
+The Lean kernel can compare expressions of type {lean}`Float` for syntactic equality, so {lean  (type := "Float")}`0.0` is definitionally equal to itself.
 ```lean
 example : (0.0 : Float) = (0.0 : Float) := by rfl
 ```
 
 Terms that require reduction to become syntactically equal cannot be checked by the kernel:
-```lean (error := true) (name := zeroPlusZero)
+```lean +error (name := zeroPlusZero)
 example : (0.0 : Float) = (0.0 + 0.0 : Float) := by rfl
 ```
 ```leanOutput zeroPlusZero
@@ -63,7 +63,7 @@ is not definitionally equal to the right-hand side
 ```
 
 Similarly, the kernel cannot evaluate {lean}`Bool`-valued comparisons of floating-point numbers while checking definitional equality:
-```lean (error := true) (name := zeroPlusZero') (keep := false)
+```lean +error (name := zeroPlusZero') -keep
 theorem Float.zero_eq_zero_plus_zero :
     ((0.0 : Float) == (0.0 + 0.0 : Float)) = true :=
   by rfl
@@ -141,7 +141,7 @@ is syntactic sugar for
 (OfScientific.ofScientific 41352 true 2 : Float32)
 ```
 
-```lean (show := false)
+```lean -show
 example : (-2.2523 : Float) = (Neg.neg (OfScientific.ofScientific 22523 true 4) : Float) := by simp [OfScientific.ofScientific]
 example : (413.52 : Float32) = (OfScientific.ofScientific 41352 true 2 : Float32) := by simp [OfScientific.ofScientific]
 ```