### Referencing Subproofs and Initial Setup

Source: https://github.com/cpitclaudel/alectryon/blob/main/recipes/references.rst

Examples of referencing subproofs and the initial setup within a Coq code block, showing continuity of counters.

```rst
- Bullets (``-``, ``+``, ``*``) delimit subproofs (:mref:`.io#setup.s(Base case)`, :mref:`Induction`)
- It all started at :mref:`.io#setup.s(Fixpoint).in`
```

--------------------------------

### JSON Input Example

Source: https://github.com/cpitclaudel/alectryon/blob/main/README.rst

Example of a JSON file containing Coq fragments for Alectryon processing.

```json
["Example xyz (H: False): True. (* ... *) exact I. Qed.",
 "Print xyz."]
```

--------------------------------

### Path Examples for Proof Elements

Source: https://github.com/cpitclaudel/alectryon/blob/main/README.rst

Provides examples of paths used to select specific elements within a Coq proof, such as sentences, goals, and hypotheses.

```rst
- ``[α]``

  ``.s(Goal ∀)``
     Search for a sentence (``.s(…)``) by matching its contents.
```

```rst
- ``[β]``

  ``.s(Base case).ccl``
     Search for a sentence (``.s(…)``) matching ``Base case``, then match the conclusion (``.ccl``) of its first goal.
```

```rst
- ``[γ]``

  ``.s(Induction).h#IHm``
     Search for a sentence (``.s(…)``) matching ``Induction``, then match the hypothesis ``IHm`` by name  (``.h#…``) in the first goal.

  ``.s(Induction).g#1.h(m + n = n + m)``
     Search for a sentence (``.s(…)``) matching ``Induction``, select its first goal by number (``.g#…``), match the hypothesis ``IHm`` by searching for its contents (``.h(…)``).
```

--------------------------------

### Lean 3: Using the 'contra' Tactic in an Example Proof

Source: https://github.com/cpitclaudel/alectryon/blob/main/recipes/_output/lean3-tutorial.html

This example demonstrates how to use the 'contra' tactic to prove a theorem involving propositional logic. The 'by contra' command invokes the tactic.

```Lean
example (p q r : Prop) (h₁ : p ∧ q) (h₂ : q → r) (h₃ : ¬ (p ∧ q)) : r :=
  by contra
```

--------------------------------

### Marker-Placement Mini-Language Examples

Source: https://github.com/cpitclaudel/alectryon/blob/main/README.rst

Illustrates the use of the marker-placement mini-language for precise control over displayed proof elements.

```rst
``-.h(Inhabited)``
  Hide all hypotheses that mention ``Inhabited``
```

```rst
``-.g#2.h#IHn``
  Hide hypothesis ``IHn`` in goal 2.
```

```rst
``-.g#2.h#*``
  Hide all hypotheses of goal 2.
```

```rst
``-.h#* .h#IHn``
  Show only hypothesis ``IHn``
```

```rst
``-.g#* .g#1 .g#3 .g{False}``
  Show only goals 1, 3, and any goal whose conclusion is ``False``.
```

```rst
``.msg[lang]=haskell``
  Highlight the bodies of all messages produced by this sentence using the Haskell lexer.
```

--------------------------------

### Lean 3 Trivial Tactic with Begin Block Example

Source: https://github.com/cpitclaudel/alectryon/blob/main/recipes/_output/tests/corner_cases.lean3.html

Demonstrates using `try begin trivial end`.

```Lean
example : true := by

* * *

true begin

* * *

true

  try begin trivial end
```

--------------------------------

### Lean 3 Conjunction Example

Source: https://github.com/cpitclaudel/alectryon/blob/main/recipes/_output/tests/corner_cases.lean3.html

Example demonstrating how to prove a conjunction of three propositions using `split`.

```Lean
example (p q r : Prop) (hp : p) (hq : q) (hr : r) :
  p ∧ q ∧ r :=
begin

p, q, r**:** Prop  
hp**:** p  
hq**:** q  
hr**:** r  

* * *

p ∧ q ∧ r

  split,
```

```Lean
p, q, r**:** Prop  
hp**:** p  
hq**:** q  
hr**:** r  

* * *

p
```

```Lean
p, q, r**:** Prop  
hp**:** p  
hq**:** q  
hr**:** r  

* * *

q ∧ r
```

```Lean
all_goals { try { split } },
```

```Lean
p, q, r**:** Prop  
hp**:** p  
hq**:** q  
hr**:** r  

* * *

p
```

```Lean
p, q, r**:** Prop  
hp**:** p  
hq**:** q  
hr**:** r  

* * *

q
```

```Lean
p, q, r**:** Prop  
hp**:** p  
hq**:** q  
hr**:** r  

* * *

r
```

```Lean
all_goals { assumption }
```

--------------------------------

### Lean 3 Trivial Tactic Example

Source: https://github.com/cpitclaudel/alectryon/blob/main/recipes/_output/tests/corner_cases.lean3.html

Shows how to use the `skip` and `trivial` tactics.

```Lean
example :true := begin

* * *

true

  skip,
```

```Lean
* * *

true skip; trivial
```

--------------------------------

### Lean3 Proof Documentation: Introduction to iff.intro

Source: https://github.com/cpitclaudel/alectryon/blob/main/recipes/_output/literate_lean3.html

Demonstrates documenting a Lean3 proof step using `apply iff.intro` to start proving an iff statement.

```lean
example (p q r : Prop) : p ∧ q ↔ q ∧ p :=
  apply iff.intro,
```

--------------------------------

### Coq Setup for References

Source: https://github.com/cpitclaudel/alectryon/blob/main/recipes/references.rst

A basic Coq code snippet demonstrating a Fixpoint definition and its proof structure, used as a target for marker references.

```coq
Fixpoint plus_comm (n m: nat) {struct n} : n + m = m + n.
Proof.
  destruct n eqn:Heq. (* .unfold *)
  - (* Base case *)
    rewrite <- plus_n_O; reflexivity.

```

--------------------------------

### Lean 3 Induction Tactic Example

Source: https://github.com/cpitclaudel/alectryon/blob/main/recipes/_output/tests/corner_cases.lean3.html

Demonstrates using the `induction` tactic with `skip` and `trivial`.

```Lean
-- special notation
example (n : nat) : true :=
   by

n**:** ℕ  

* * *

true induction n ; [skip, skip]; [trivial, trivial]
```

--------------------------------

### Alectryon Coq Example with Proof and Comments

Source: https://github.com/cpitclaudel/alectryon/blob/main/recipes/tests/errors.rst

A Coq example within Alectryon that includes a proof, variable assignment, and extensive multi-line comments. This snippet showcases handling of complex code structures and comments.

```coq
Goal True.
  pose proof 1 as n.
  exact I. (* A very long line *) (* whose contents are split *) (* across *) (* multiple *) (* comments *)
Qed.
```

--------------------------------

### Lean 3 Tactic Choice Example

Source: https://github.com/cpitclaudel/alectryon/blob/main/recipes/_output/tests/corner_cases.lean3.html

Illustrates using `done <|> done <|> trivial` for tactic choice.

```Lean
-- grouped as done <|> (done <|> trivial)
example : true := by

* * *

true done <|> done <|> trivial
```

--------------------------------

### Coq Example with Multiple Flags and Nested Structures

Source: https://github.com/cpitclaudel/alectryon/blob/main/recipes/display_flags.rst

Complex Coq example demonstrating various flags like 'none', 'unfold', 'in', 'messages', and handling of nested goals and proofs. It shows how different flags control the visibility of execution details.

```coq
Require PeanoNat.     (* ← Executed but hidden *) (* .none *)
Goal True.            (* ← Goal unfolded *) (* .unfold *)
  Fail exact 1.       (* ← Goal omitted *) (* .in .messages *)
  Fail fail.          (* ← Error message shown, input hidden *) (* .unfold .messages *)
  exact I.            (* ← Executed but hidden *) (* -.s{*} *)
Qed.
```

--------------------------------

### MQuote Directive Example

Source: https://github.com/cpitclaudel/alectryon/blob/main/recipes/minimal.rst

This directive is used for quoting expressions, specifically demonstrating the 'Print' command in this example.

```coq
.s(Print).in
```

--------------------------------

### Lean 3 Inequality Transitivity Example

Source: https://github.com/cpitclaudel/alectryon/blob/main/recipes/_output/tests/corner_cases.lean3.html

Demonstrates proving `k - m <= k - n` given `n <= m` using induction and `le_trans`.

```Lean
theorem sub_le_sub_left {n m : ℕ} (k) (h : n ≤ m) : k - m ≤ k - n :=
begin

n, m, k**:** ℕ  
h**:** n ≤ m  

* * *

k - m ≤ k - n

  induction h; [refl, exact le_trans (nat.pred_le _) h_ih]
```

--------------------------------

### Documenting a proof in Lean3

Source: https://github.com/cpitclaudel/alectryon/blob/main/recipes/_output/literate_lean3.lean3.rst

Example of documenting a proof in Lean3, showing goal progression and hypothesis capture. Uses .none and .unfold flags for display control.

```lean3
example (p q r : Prop) : p ∧ q ↔ q ∧ p :=
begin /- .none -/
  apply iff.intro, { 
    intro H,
    apply and.intro, /- .unfold -/
    apply (and.elim_right H),
    apply (and.elim_left H),
  }, { 
    intro H,
    apply and.intro,
    apply (and.elim_right H),
    apply (and.elim_left H),
  }
end
```

--------------------------------

### Lean 3 Tactic Sequencing Example

Source: https://github.com/cpitclaudel/alectryon/blob/main/recipes/_output/tests/corner_cases.lean3.html

Shows a sequence of tactics including `trivial` and `done`.

```Lean
-- unexecuted tactic at end
example : true := by

* * *

true {

* * *

true trivial ; done }
```

--------------------------------

### Lean 3 Propositional Logic Example

Source: https://github.com/cpitclaudel/alectryon/blob/main/recipes/_output/tests/corner_cases.lean3.html

Demonstrates basic propositional logic in Lean 3, including conjunctions and disjunctions.

```Lean
hq**:** q  
hpq**:** p ∧ q  

* * *

p ∧ q ∨ p ∧ r
```

```Lean
p, q, r**:** Prop  
hp**:** p  
hq**:** q  
hpq**:** p ∧ q  

* * *

p ∧ q exact hpq }
```

```Lean
have hpr : p ∧ r,
```

```Lean
p, q, r**:** Prop  
hp**:** p  
hr**:** r  
hpr**:** p ∧ r  

* * *

p ∧ r
```

```Lean
split ; assumption,
```

```Lean
p, q, r**:** Prop  
hp**:** p  
hr**:** r  
hpr**:** p ∧ r  

* * *

p ∧ q ∨ p ∧ r
```

```Lean
right,
```

```Lean
p, q, r**:** Prop  
hp**:** p  
hr**:** r  
hpr**:** p ∧ r  

* * *

p ∧ r
```

```Lean
exact hpr
```

--------------------------------

### Coq Computation Example

Source: https://github.com/cpitclaudel/alectryon/blob/main/recipes/sphinx/_build/html/coqchapter.html

Demonstrates a computation within a Coq file. This snippet shows how to define and evaluate a simple function in Coq.

```Coq
Compute ((fun (n: nat) (opt: option nat) (eq: opt = Some n) => n)
           \_ (Some 3) eq_refl).
```

--------------------------------

### Lean 3 Tactic Repetition Example

Source: https://github.com/cpitclaudel/alectryon/blob/main/recipes/_output/tests/corner_cases.lean3.html

Demonstrates using `repeat` with `split` and `assumption` tactics.

```Lean
example (p q r : Prop) (hp : p) (hq : q) (hr : r) :
  p ∧ q ∧ r :=
begin

p, q, r**:** Prop  
hp**:** p  
hq**:** q  
hr**:** r  

* * *

p ∧ q ∧ r

  repeat { all_goals { split <|> assumption } }
```

--------------------------------

### Coq Definition and Print Example

Source: https://github.com/cpitclaudel/alectryon/blob/main/recipes/sphinx/index.rst

Demonstrates defining a Coq function and then printing its definition. Use '.unfold' to expand definitions and '.no-goals' to suppress goal display during proof.

```coq
Definition example_from_sphinx: nat. (* .unfold *)
Proof. (* .no-goals *)
  simple apply Nat.add.
  exact 1.
  assert (n: nat).
  2: clear n.
  exact 3.
  exact 2.
Defined.

Print example_from_sphinx. (* .unfold *)
```

--------------------------------

### Coq Named Goal Example

Source: https://github.com/cpitclaudel/alectryon/blob/main/recipes/tests/literate.rst

Demonstrates how to name a Coq goal using the ':name:' attribute. This is useful for referring to specific goals later in a proof.

```coq
exact I.
```

--------------------------------

### Lean 3 Nested Tactic Blocks Example

Source: https://github.com/cpitclaudel/alectryon/blob/main/recipes/_output/tests/corner_cases.lean3.html

Illustrates nested tactic blocks with `skip` and `[skip, skip]`.

```Lean
example : true := by

* * *

true {

* * *

true {{{{ skip ; [skip, skip] }}}} <|> trivial}
```

--------------------------------

### Coq Goal with Leading Blanks

Source: https://github.com/cpitclaudel/alectryon/blob/main/recipes/sphinx/_build/html/corner_cases.html

Demonstrates a simple Coq goal where the code starts with blank lines.

```coq
Goal True.

exact I.
Qed.
```

--------------------------------

### Setup Alectryon Docutils Extensions

Source: https://github.com/cpitclaudel/alectryon/blob/main/README.rst

Include this code in your configuration file to set up Alectryon's docutils extensions for directives and roles.

```python
import alectryon.docutils
alectryon.docutils.setup()
```

--------------------------------

### Lean3 Proof Documentation: Applying and.intro

Source: https://github.com/cpitclaudel/alectryon/blob/main/recipes/_output/literate_lean3.html

Shows documenting a Lean3 proof step using `apply and.intro` within a proof.

```lean
    apply and.intro,
```

--------------------------------

### Customizing Proof Rendering with Directives

Source: https://github.com/cpitclaudel/alectryon/blob/main/recipes/references.rst

Customize proof rendering by omitting hypotheses based on name or type, and filtering goals. This example shows omitting hypotheses starting with 'l' or named 'a'/'A', and then filtering to specific goals.

```rst
.. coq:: -.h#l* -.h#[aA] -.s(Check let).msg(let) -.s{Proof.}
   :name: pr

   Require Import Coq.Sorting.Permutation. (* .none *)
   Check let t := nat in forall n: t, n >= 0. (* .unfold *)
   Theorem Permutation_In {A} (l l' : list A) (a: A) :
     Permutation l l' -> List.In a l -> List.In a l'. (* .unfold *)
   Proof.
     induction 1; intros * Hin; [ | refine ?[gg] | .. ].
       (* .unfold -.g#* .g#2 .g#4 .g#4.h{list A} *)
   all: simpl in *; tauto.
   Qed.
```

--------------------------------

### Annotate Larger Coq Example with Arguments

Source: https://github.com/cpitclaudel/alectryon/blob/main/recipes/api.rst

Annotates a list of Coq fragments using `annotate` with custom `vsrocq_args`. The output is pretty-printed for readability.

```python
from alectryon.vsrocq import annotate
fragments = ["Check 1.", "Goal False -> True. intros H."]
annotated = annotate(fragments, vsrocq_args=('-Q', libdir, 'lib'))
pprint(annotated, width=65)
```

--------------------------------

### Lean 3 Nested Tactic Blocks with Tactic Choice Example

Source: https://github.com/cpitclaudel/alectryon/blob/main/recipes/_output/tests/corner_cases.lean3.html

Shows nested tactic blocks with `skip` and tactic choice.

```Lean
example : true := begin

* * *

true {

* * *

true {{{{ skip ; [skip, skip] }}}} <|> trivial} end
```

--------------------------------

### Scheme code example

Source: https://github.com/cpitclaudel/alectryon/blob/main/recipes/_output/references.html

An example of Scheme code produced by Extraction.

```scheme
(define add (lambdas (n m)
  (match n
     ((O) m)
     ((S p) `(S ,(@ add p m))))))
```

--------------------------------

### Lean 3 Tactic Choice with Skip and Brackets Example

Source: https://github.com/cpitclaudel/alectryon/blob/main/recipes/_output/tests/corner_cases.lean3.html

Shows tactic choice using `<|>` with `skip` and `[skip, skip]`.

```Lean
example : true := by

* * *

true {

* * *

true { skip ; [skip, skip] } <|> trivial}
```

--------------------------------

### Lean 3 Tactic Choice with Nested Skip and Brackets Example

Source: https://github.com/cpitclaudel/alectryon/blob/main/recipes/_output/tests/corner_cases.lean3.html

Illustrates tactic choice with nested `skip` and `[skip, skip]`.

```Lean
example : true := begin

* * *

true {

* * *

true { skip ; [skip, skip] } <|> trivial} end
```

--------------------------------

### Failing Definition Example

Source: https://github.com/cpitclaudel/alectryon/blob/main/recipes/_output/display_flags.html

An example of a definition that is expected to fail due to a type error.

```coq
Definition a :=
  (* `.fails` adds red highlight and removes "indeed failed". *)
  1 + true.
```

--------------------------------

### JSON Output Example

Source: https://github.com/cpitclaudel/alectryon/blob/main/README.rst

Example of JSON output generated by Alectryon when using the `json` backend.

```json
[ // A list of processed fragments
  [ // Each fragment is a list of records
    { // Each record has a type, and type-specific fields
      "_type": "sentence",
      "sentence": "Example xyz (H: False): True.",
      "responses": [],
      "goals": [ { "_type": "goal",
                   "name": "2",
                   "conclusion": "True",
                   "hypotheses": [ { "_type": "hypothesis",
                                     "name": "H",
                                     "body": null,
                                     "type": "False" } ] } ] },
    {"_type": "text", "string": " (* ... *) "},
    {"_type": "sentence", "sentence": "exact I.", "responses": [], "goals": []},
    {"_type": "text", "string": " "},
    {"_type": "sentence", "sentence": "Qed.", "responses": [], "goals": []} ],
  [
    { "_type": "sentence",
      "sentence": "Print xyz.",
      "responses": ["xyz = fun _ : False => I\n     : False -> True"],
      "goals": [] } ] ]
```

--------------------------------

### Lean3 Proof Documentation: Using and.elim_right

Source: https://github.com/cpitclaudel/alectryon/blob/main/recipes/_output/literate_lean3.html

Demonstrates documenting a Lean3 proof step using `apply (and.elim_right H)` to extract a component from a conjunction.

```lean
    apply (and.elim_right H),
```

--------------------------------

### Lean3 Proof Documentation: Completing a Proof with iff.intro

Source: https://github.com/cpitclaudel/alectryon/blob/main/recipes/_output/literate_lean3.html

Illustrates the completion of a Lean3 proof for an iff statement, including the use of `apply iff.intro`.

```lean
  }, { 

> p, q, r**:** Prop  
> 
> * * *
> 
> q ∧ p → p ∧ q

    intro H,

> p, q, r**:** Prop  
> H**:** q ∧ p  
> 
> * * *
> 
> p ∧ q

    apply and.intro,

> p, q, r**:** Prop  
> H**:** q ∧ p  
> 
> * * * 
> 
> p

> p, q, r**:** Prop  
> H**:** q ∧ p  
> 
> * * *
> 
> q

    apply (and.elim_right H),

> p, q, r**:** Prop  
> H**:** q ∧ p  
> 
> * * *
> 
> q

    apply (and.elim_left H),
  }
```

--------------------------------

### Alectryon Coq Example with Inapplicable Targets

Source: https://github.com/cpitclaudel/alectryon/blob/main/recipes/tests/errors.rst

Illustrates inapplicable targets in Alectryon's Coq environment, showing various scenarios where targets are not found or are incorrectly specified. This tests dynamic target resolution and error reporting.

```coq
Check nat. (* .io#abc *)
Check nat. (* .g#1 *)
Goal True. (* .g#1.ccl .in .g#1.name *)
  idtac. (* .g#1.h{*}.body .g#1.h{*}.type .g#1.h{*}.name *)
Abort. (* .msg{*} *)
```

--------------------------------

### Theorem Proof with Intro and Exact (Begin/End Block)

Source: https://github.com/cpitclaudel/alectryon/blob/main/recipes/_output/tests/corner_cases.lean3.html

An alternative way to write the previous theorem proof using `begin`/`end` block, demonstrating `intro` and `exact`.

```lean
theorem t1 : true -> true :=
  begin

> * * *
> 
> true → true

    -- ⊢ true → true    intro,

> ᾰ**:** true  
> 
> * * *
> 
> true

    -- ᾰ : true ⊢ true    exact true.intro
  end
```

--------------------------------

### Example of custom counter style usage

Source: https://github.com/cpitclaudel/alectryon/blob/main/recipes/_output/references.html

Illustrates the output of custom counter styles, showing references to an identifier, its definition, and the type/reduction of a term.

```coq
The following commands print information about an identifier [α](#references-rst-io-cp-s-about-0), print its definition [β](#references-rst-io-cp-s-print-0), and compute the type of a term [γ](#references-rst-io-cp-s-check-0) or its reduction [δ](#references-rst-io-cp-s-compute-0).

About Nat.add.α

> Nat.add : nat -> nat -> nat
> 
> Nat.add is not universe polymorphic
> Arguments Nat.add (n m)%_nat_scope
```

--------------------------------

### Coq Proof with Subproofs and References

Source: https://github.com/cpitclaudel/alectryon/blob/main/recipes/references.rst

A Coq proof snippet that includes subproofs delimited by bullets, and references to the initial setup and subproofs.

```coq
- (* Induction *)
  simpl.
  rewrite (plus_comm n0).
  rewrite plus_n_Sm.
  reflexivity.
Qed.
```

--------------------------------

### Tagging Code with Properties

Source: https://github.com/cpitclaudel/alectryon/blob/main/recipes/references.rst

Example of adding custom properties like `[foo]=bar` to code markers, and how Alectryon uses the `[lang]` annotation for syntax highlighting.

```coq
Check nat. (* .in[foo]=bar *)
```

--------------------------------

### Alectryon Coq Example with Inconsistent Flags

Source: https://github.com/cpitclaudel/alectryon/blob/main/recipes/tests/errors.rst

Shows an example of inconsistent flags in Alectryon's Coq environment. This snippet tests the detection of conflicting flag usage.

```coq
Check nat. (* .fold *)
```

--------------------------------

### Lean3 Proof Documentation: Using and.elim_left

Source: https://github.com/cpitclaudel/alectryon/blob/main/recipes/_output/literate_lean3.html

Shows documenting a Lean3 proof step using `apply (and.elim_left H)` to extract a component from a conjunction.

```lean
    apply (and.elim_left H),
```

--------------------------------

### Coq Proof Step: Check and Type

Source: https://github.com/cpitclaudel/alectryon/blob/main/recipes/api.rst

An example of a Coq interaction showing a 'Check' command and its output, which includes the type of the checked term.

```coq
\begin{alectryon}
  \begin{\al{sentence}}
    \begin{\al{input}}
      \PY{k+kn}{Check}~\PY{l+m+mi}{1}\PY{o}{.}
    \end{\al{input}}
    \Al{sep}
    \begin{\al{output}}
      \begin{\al{messages}}
        \begin{\al{message}}
          \PY{l+m+mi}{1}\Al{nl}
          ~~~~~\PY{o}{:}~\PY{n}{nat}
        \end{\al{message}}
      \end{\al{messages}}
    \end{\al{output}}
  \end{\al{sentence}}
\end{alectryon}
```

--------------------------------

### Coq Example within Body-Only Output

Source: https://github.com/cpitclaudel/alectryon/blob/main/recipes/tests/body_only.rst

Demonstrates a Coq code snippet that would be included in the body-only output. This shows how code blocks are rendered when the --body-only flag is used.

```coq
Print nat.

```

--------------------------------

### Coq Proof Step: All Intros

Source: https://github.com/cpitclaudel/alectryon/blob/main/recipes/_output/literate_reST.html

Introduces all variables and hypotheses into the context for the current Coq goal. This is often used after a tactic like 'revert' or 'induction'.

```Coq
all: intros x z (Hl & Hr).
```

--------------------------------

### Documenting Proof Steps in Lean4

Source: https://github.com/cpitclaudel/alectryon/blob/main/recipes/_output/literate_lean4.html

This snippet shows how Alectryon captures the state of a Lean4 proof, including goals and hypotheses, as the proof progresses. It demonstrates applying tactics like 'apply Iff.intro'.

```lean
theorem test (p q : Prop) (hp : p) (hq : q): p ∧ q ↔ q ∧ p := by

> p, q**:** Prop  
> hp**:** p  
> hq**:** q  
> 
> * * *
> 
> p ∧ q ↔ q ∧ p

  apply Iff.intro

> p, q**:** Prop  
> hp**:** p  
> hq**:** q  
> 
> * * *
> 
> mp
> 
> p ∧ q → q ∧ p

> p, q**:** Prop  
> hp**:** p  
> hq**:** q  
> 
> * * *
> 
> mpr
> 
> q ∧ p → p ∧ q

  .

> p, q**:** Prop  
> hp**:** p  
> hq**:** q  
> 
> * * *
> 
> mp
> 
> p ∧ q → q ∧ p intro h

> p, q**:** Prop  
> hp**:** p  
> hq**:** q  
> h**:** p ∧ q  
> 
> * * *
> 
> mp
> 
> q ∧ p

    apply And.intro

> p, q**:** Prop  
> hp**:** p  
> hq**:** q  
> h**:** p ∧ q  
> 
> * * *
> 
> mp.left
> 
> q

> p, q**:** Prop  
> hp**:** p  
> hq**:** q  
> h**:** p ∧ q  
> 
> * * *
> 
> mp.right
> 
> p

    .

> p, q**:** Prop  
> hp**:** p  
> hq**:** q  
> h**:** p ∧ q  
> 
> * * *
> 
> mp.left
> 
> q exact hq

> * * * 
> 
> Goals accomplished! 🐙

    .

> p, q**:** Prop  
> hp**:** p  
> hq**:** q  
> h**:** p ∧ q  
> 
> * * *
> 
> mp.right
> 
> p exact hp

> * * *
> 
> Goals accomplished! 🐙

  .

> p, q**:** Prop  
> hp**:** p  
> hq**:** q  
> 
> * * *
> 
> mpr
> 
> q ∧ p → p ∧ q intro h

> p, q**:** Prop  
> hp**:** p  
> hq**:** q  
> h**:** q ∧ p  
> 
> * * *
> 
> mpr
> 
> p ∧ q

    apply And.intro

> p, q**:** Prop  
> hp**:** p  
> hq**:** q  
> h**:** q ∧ p  
> 
> * * *
> 
> mpr.left
> 
> p

> p, q**:** Prop  
> hp**:** p  
> hq**:** q  
> h**:** q ∧ p  
> 
> * * *
> 
> mpr.right
> 
> q

    .

> p, q**:** Prop  
> hp**:** p  
> hq**:** q  
> h**:** q ∧ p  
> 
> * * *
> 
> mpr.left
> 
> p exact hp

> * * *
> 
> Goals accomplished! 🐙

    .

> p, q**:** Prop  
> hp**:** p  
> hq**:** q  
> h**:** q ∧ p  
> 
> * * *
> 
> mpr.right
> 
> q exact hq

> * * *
> 
> Goals accomplished! 🐙
```

--------------------------------

### Coq Exercise Directive

Source: https://github.com/cpitclaudel/alectryon/blob/main/recipes/sphinx/_build/html/corner_cases.html

Example of using the 'Exercise' directive in Coq.

```coq
Exercise: Commutativity of addition

Goal forall x y: nat, x + y = y + x.
Abort.
```

--------------------------------

### Coq Goal Manipulation

Source: https://github.com/cpitclaudel/alectryon/blob/main/recipes/_output/tests/goal_names.v.html

Example of destructing a boolean goal and refining it.

```coq
destruct b; [ refine ?[true] | refine ?[false] ].
all: reflexivity.
```

--------------------------------

### Coq Proof Step: Goal and Introduction

Source: https://github.com/cpitclaudel/alectryon/blob/main/recipes/api.rst

Demonstrates a Coq proof scenario where a goal is stated (False -> True) and then an hypothesis 'H' is introduced.

```coq
\begin{alectryon}
  \begin{\al{sentence}}
    \begin{\al{input}}
      \PY{k+kn}{Goal}~\PY{k+kt}{False}~\PY{o}{\PYZhy{}\PYZgt{}}~\PY{k+kt}{True}\PY{o}{.}
    \end{\al{input}}
    \Al{sep}
    \begin{\al{output}}
      \begin{\al{goals}}
        \begin{\al{goal}}
          \begin{\al{hyps}}\end{\al{hyps}}
          \Al{sep}
          \Al{infrule}{}
          \Al{sep}
          \begin{\al{conclusion}}
            \PY{k+kt}{False}~\PY{o}{\PYZhy{}\PYZgt{}}~\PY{k+kt}{True}
          \end{\al{conclusion}}
        \end{\al{goal}}
      \end{\al{goals}}
    \end{\al{output}}
  \end{\al{sentence}}
  \Al{sep}
  \begin{\al{sentence}}
    \begin{\al{input}}
      \PY{n+nb}{intros}~\PY{n}{H}\PY{o}{.}
    \end{\al{input}}
    \Al{sep}
    \begin{\al{output}}
      \begin{\al{goals}}
        \begin{\al{goal}}
          \begin{\al{hyps}}
            \Al{hyp}{H}{\PY{k+kt}{False}}
          \end{\al{hyps}}
          \Al{sep}
          \Al{infrule}{}
          \Al{sep}
          \begin{\al{conclusion}}
            \PY{k+kt}{True}
          \end{\al{conclusion}}
        \end{\al{goal}}
      \end{\al{goals}}
    \end{\al{output}}
  \end{\al{sentence}}
\end{alectryon}
```

--------------------------------

### MyST Coq Fragment Example

Source: https://github.com/cpitclaudel/alectryon/blob/main/recipes/_output/literate_MyST.html

Demonstrates how to embed Coq code within MyST Markdown using ```{coq} syntax. Arguments are on the same line, and options are below.

```coq
Goal exists x, x * x = 49 /\ x < 10.
```

```coq
exists x : nat, x * x = 49 /\ x < 10
```

```coq
let rec t n := (exists n; split; [reflexivity |]) || t (S n) in t 0.
```

```coq
7 < 10
```

```coq
unfold lt.
```

```coq
8 <= 10
```

```coq
repeat constructor.
```

--------------------------------

### Asserting Properties of Output with .. coq::

Source: https://github.com/cpitclaudel/alectryon/blob/main/recipes/references.rst

Use the .. coq:: directive to display code and assert properties of its output. This example shows a basic 'Print plus.' command.

```rst
.. coq::
   :name: plus

   Print plus.
```

--------------------------------

### Theorem Proof with Repeat Intro and Admit

Source: https://github.com/cpitclaudel/alectryon/blob/main/recipes/_output/tests/corner_cases.lean3.html

Demonstrates proving a theorem using `repeat { intro }` and `admit` to pause the proof.

```lean
theorem t4 : true -> true -> true :=
  by

> * * *
> 
> true → true → true {

> * * *
> 
> true → true → true repeat { intro },

> ᾰ, ᾰ_1**:** true  
> 
> * * *
> 
> true admit }

```

--------------------------------

### Variable Definition Example

Source: https://github.com/cpitclaudel/alectryon/blob/main/recipes/_output/display_flags.html

Defines a simple variable 'xyz' with a numeric value.

```coq
Definition xyz := 123.
```

--------------------------------

### Interactive Proof Step: Intros

Source: https://github.com/cpitclaudel/alectryon/blob/main/recipes/_output/tests/screenshot.html

Introduces variables and uses an injection pattern in an interactive theorem proving session.

```Coq
intros x y [=Heq].
```

--------------------------------

### Evaluate Lean3 expression

Source: https://github.com/cpitclaudel/alectryon/blob/main/recipes/_output/literate_lean3.lean3.rst

Example of reducing a Lean3 expression. Results are captured by Alectryon.

```lean3
#reduce let x := 5 in x + 3
```

--------------------------------

### Compile Lean 3 Tutorial to Lean 3

Source: https://github.com/cpitclaudel/alectryon/blob/main/recipes/lean3-tutorial.rst

Compiles a reStructuredText file with Lean 3 code into a Lean 3 file.

```bash
alectryon lean3-tutorial.rst -o lean3-tutorial.lean3
    # reST+Lean → Lean; produces ‘lean3-tutorial.lean3’
```

--------------------------------

### Undefined Reference Error Example

Source: https://github.com/cpitclaudel/alectryon/blob/main/recipes/_output/display_flags.html

Shows an error when defining a variable with an undefined reference.

```coq
Definition a := asd.
```

--------------------------------

### Generate Webpage from Literate Coq File

Source: https://github.com/cpitclaudel/alectryon/blob/main/README.rst

Compile a literate Coq file into an interactive webpage. The first command uses default settings, while the second explicitly sets the frontend and backend.

```bash
alectryon literate_coq.v
alectryon --frontend coq+rst --backend webpage literate_coq.v -o literate_coq.html
```

--------------------------------

### Run Alectryon with Coq Minification

Source: https://github.com/cpitclaudel/alectryon/blob/main/recipes/_output/tests/minification.v.html

Command-line instruction to process a Coq file using Alectryon with HTML minification enabled.

```bash
alectryon --frontend coq --html-minification minification.v
```

--------------------------------

### Lean 3 Trivial Tactic with Try Example

Source: https://github.com/cpitclaudel/alectryon/blob/main/recipes/_output/tests/corner_cases.lean3.html

Shows using `try` with `trivial` tactic.

```Lean
example : true := by

* * *

true {

* * *

true

  try { trivial }
```

--------------------------------

### Theorem Proof with Intro and Exact

Source: https://github.com/cpitclaudel/alectryon/blob/main/recipes/_output/tests/corner_cases.lean3.html

Proves an implication theorem using `intro` to handle the implication and `exact` to provide the proof.

```lean
theorem t0 : true -> true :=
  by

> * * *
> 
> true → true {

> * * *
> 
> true → true intro,

> ᾰ**:** true  
> 
> * * *
> 
> true exact true.intro }
```

--------------------------------

### Compile Lean 3 Tutorial to HTML

Source: https://github.com/cpitclaudel/alectryon/blob/main/recipes/lean3-tutorial.rst

Compiles a reStructuredText file with Lean 3 code into an HTML file.

```bash
alectryon lean3-tutorial.rst
    # reST+Lean → HTML; produces ‘lean3-tutorial.html’
```

--------------------------------

### Coq Print Nat Message Role

Source: https://github.com/cpitclaudel/alectryon/blob/main/recipes/_output/minimal.no-alectryon.html

Example of a Coq 'Print.msg' role with 'nat' as an argument.

```Coq
.s(Print).msg{*nat*}
```

--------------------------------

### Generate Webpage from Plain Coq File

Source: https://github.com/cpitclaudel/alectryon/blob/main/README.rst

Compile a plain Coq file into an interactive webpage. The first command uses default settings, while the second explicitly sets the frontend and backend.

```bash
alectryon --frontend coq plain.v
alectryon --frontend coq --backend webpage plain.v -o plain.v.html
```

--------------------------------

### Type Mismatch Error Example

Source: https://github.com/cpitclaudel/alectryon/blob/main/recipes/_output/display_flags.html

Illustrates a type mismatch error when checking '1 + true'.

```coq
Check 1 + true.
```

--------------------------------

### Proof Step: Try Constructor

Source: https://github.com/cpitclaudel/alectryon/blob/main/recipes/_output/coqdoc.html

A step in the Coq proof, attempting to use the 'constructor' tactic.

```Coq
all: try constructor.
```

--------------------------------

### Lean 3 Skip and Trivial Tactic Example

Source: https://github.com/cpitclaudel/alectryon/blob/main/recipes/_output/tests/corner_cases.lean3.html

Shows `skip` and `trivial` tactics with a trailing comma.

```Lean
example : true := begin

* * *

true
skip,

* * *

trivial, -- trailing comma
end
```

--------------------------------

### Lean 3 Arithmetic Transitivity Example

Source: https://github.com/cpitclaudel/alectryon/blob/main/recipes/_output/tests/corner_cases.lean3.html

Proves transitivity of equality for natural numbers using `rw`.

```Lean
example (n m k : ℕ) (h1 : n \= m) (h2 : m \= k): (n \= k) :=
begin

n, m, k**:** ℕ  
h1**:** n \= m  
h2**:** m \= k  

* * *

n \= k

    rw [show n \= m, by assumption, show m \= k, by assumption]
```

--------------------------------

### Coq Hidden Code Example

Source: https://github.com/cpitclaudel/alectryon/blob/main/recipes/display_flags.rst

A simple Coq code block marked as hidden, with the 'none' flag.

```coq
(* Hidden *)
```

--------------------------------

### Coq Proof Step: Intros and Revert

Source: https://github.com/cpitclaudel/alectryon/blob/main/recipes/_output/literate_reST.html

Introduces variables x and y, then reverts x and performs induction on y as a proof strategy for the current Coq goal.

```Coq
intros x y.
  revert x; induction y.
```

--------------------------------

### Lean3 Code: Checking Type of bool

Source: https://github.com/cpitclaudel/alectryon/blob/main/recipes/_output/literate_lean3.html

Example of using `#check` in Lean3 to inspect the type of 'bool'.

```lean
#check bool
```

--------------------------------

### Coq Lemma with 'all' flag

Source: https://github.com/cpitclaudel/alectryon/blob/main/recipes/display_flags.rst

Demonstrates a Coq lemma where all details are shown using the '.all' flag. This includes intermediate steps and potentially verbose output.

```coq
Lemma foo (t: True): True. (* .all *)
  idtac "foo". (* .no-ccls .unfold *)
Abort.
```

--------------------------------

### Lean3 Code: Checking Type of nat

Source: https://github.com/cpitclaudel/alectryon/blob/main/recipes/_output/literate_lean3.html

Example of using `#check` in Lean3 to inspect the type of 'nat'.

```lean
#check nat
```

--------------------------------

### Alectryon CLI Help

Source: https://github.com/cpitclaudel/alectryon/blob/main/README.rst

Basic command-line structure for Alectryon. Use `--help` for full details.

```bash
alectryon [-h] […]
             [--frontend {coq,coq+rst,coqdoc,html,json,md,rst,tex}]
             [--backend {coq,coq+rst,json,latex,rst,snippets-html,snippets-latex,webpage,…}]
             input [input ...]
```

--------------------------------

### Alectryon Python Library Annotation

Source: https://github.com/cpitclaudel/alectryon/blob/main/README.rst

Example of using the `annotate` function from `alectryon.vsrocq` to process Coq code chunks.

```python
from alectryon.vsrocq import annotate
annotate(["Example xyz (H: False): True. (* ... *) exact I. Qed.", "Check xyz."])
```

--------------------------------

### Compiling with Alectryon

Source: https://github.com/cpitclaudel/alectryon/blob/main/recipes/references.rst

Demonstrates basic compilation commands for Alectryon. Use this to convert ReST files to HTML or LaTeX.

```bash
$ alectryon references.rst
    # ReST \342\200\224 HTML; produces \342\200\230references.html\342\200\231
$ DOCUTILSCONFIG=references.docutils.conf alectryon \
    references.rst -o references.lua.tex --latex-dialect lualatex
    # ReST \342\200\224 LaTeX; produces \342\200\230references.lua.tex\342\200\231
```

--------------------------------

### Minimal reST to Coq via Stdin

Source: https://github.com/cpitclaudel/alectryon/blob/main/recipes/_output/literate_reST.html

Convert minimal reST input to a Coq (.v) file using alectryon.literate, reading from standard input and writing to standard output, which is then redirected to 'literate_reST.min.stdin.v'.

```bash
$ cd ..; python -m alectryon.literate --from rst --to coq - \
    < recipes/literate_reST.rst > recipes/literate_reST.min.stdin.v
  # Minimal reST → Coq; produces ‘literate_reST.min.stdin.v’
```

--------------------------------

### Lean 3 Trivial Tactic with Trailing Comma Example

Source: https://github.com/cpitclaudel/alectryon/blob/main/recipes/_output/tests/corner_cases.lean3.html

Demonstrates `trivial` tactic with a trailing comma in a block.

```Lean
-- trailing comma
example : true := by

* * *

true {

* * *

true skip ; trivial, }
```

--------------------------------

### Basic Coq Lemma and Goal

Source: https://github.com/cpitclaudel/alectryon/blob/main/recipes/literate_reST.rst

A simple Coq lemma 'le_l' and a 'Goal' demonstrating basic Coq syntax within an '.. coq::' directive.

```coq
Lemma le_l : forall y x, S x <= y -> x <= y.
  induction y; inversion 1; subst.
  all: info_eauto.
Qed.

Goal forall x y z, x <= y <= z -> x <= z.
```

--------------------------------

### Coq Visible Code Example

Source: https://github.com/cpitclaudel/alectryon/blob/main/recipes/display_flags.rst

A simple Coq code block marked as visible, with no specific flags applied.

```coq
(* Visible *)
```

--------------------------------

### Coq Definition Example

Source: https://github.com/cpitclaudel/alectryon/blob/main/recipes/_output/literate_reST.html

Defines a simple Coq string literal named 'test'. This can be referenced elsewhere in the document.

```Coq
Definition test := "Hello, World!".
```

--------------------------------

### Lean4: Documenting a Proof

Source: https://github.com/cpitclaudel/alectryon/blob/main/recipes/_output/literate_lean4.lean.rst

This Lean4 code demonstrates documenting a proof for the theorem 'test (p ∧ q ↔ q ∧ p)'. Alectryon captures goals and hypotheses as the proof progresses.

```lean4
theorem test (p q : Prop) (hp : p) (hq : q): p ∧ q ↔ q ∧ p := by
  apply Iff.intro
  . intro h
    apply And.intro
    . exact hq
    . exact hp
  . intro h
    apply And.intro
    . exact hp
    . exact hq
```

--------------------------------

### Lean3 Code: Evaluating Arithmetic Operation

Source: https://github.com/cpitclaudel/alectryon/blob/main/recipes/_output/literate_lean3.html

Example of using `#eval` in Lean3 to evaluate the sum of two numbers.

```lean
#eval 1 + 1
```

--------------------------------

### Unfold and evaluate in Lean3

Source: https://github.com/cpitclaudel/alectryon/blob/main/recipes/_output/literate_lean3.lean3.rst

Example demonstrating the use of the 'unfold' directive to display results of both #check and #eval in Lean3.

```lean3
unfold

#check bool
#eval 1 + 1
```

--------------------------------

### Unfold check result in Lean3

Source: https://github.com/cpitclaudel/alectryon/blob/main/recipes/_output/literate_lean3.lean3.rst

Example of using the .unfold flag to display the result of a #check command in Lean3.

```lean3
#check nat /- .unfold -/
```

--------------------------------

### Coq Definition and Check

Source: https://github.com/cpitclaudel/alectryon/blob/main/recipes/sphinx/corner_cases.rst

Demonstrates defining a simple value in Coq and then checking its reference using Alectryon's path resolution.

```coq
Definition a := 1.
Check corner_cases.a.
```

--------------------------------

### Referencing a Coq Fixpoint

Source: https://github.com/cpitclaudel/alectryon/blob/main/recipes/references.rst

Example of using the :mref:`search-term` syntax to automatically label and reference a Coq Fixpoint command.

```rst
The `Fixpoint` command (:mref:`Fixpoint plus_comm`) indicates that we are beginning an inductive proof.
```

--------------------------------

### Coq Proof Step: constructor; apply even_Even_fp; assumption

Source: https://github.com/cpitclaudel/alectryon/blob/main/recipes/_output/literate_coq.html

Uses 'constructor' to introduce a new case, applies the 'even_Even_fp' lemma, and uses 'assumption' to close the goal. Demonstrates recursive proof construction.

```Coq
constructor; apply even_Even_fp; assumption.
```

--------------------------------

### Coq Exercise Directive

Source: https://github.com/cpitclaudel/alectryon/blob/main/recipes/sphinx/corner_cases.rst

Example of using the 'exercise' directive in Alectryon to mark a Coq code block as an exercise with difficulty.

```coq
Goal forall x y: nat, x + y = y + x.
Abort.
```

--------------------------------

### Lean 3 Empty Tactic Block Example

Source: https://github.com/cpitclaudel/alectryon/blob/main/recipes/_output/tests/corner_cases.lean3.html

Demonstrates an empty tactic block with `trivial` and nested `skip` blocks.

```Lean
-- { } block with no executed children
-- there is no first goal to focus on
example : true := begin

* * *

true { trivial , { skip, skip } } <|> trivial end
```

--------------------------------

### Generate Webpage from Coqdoc File

Source: https://github.com/cpitclaudel/alectryon/blob/main/README.rst

Compile a Coqdoc file into an interactive webpage. The first command uses default settings, while the second explicitly sets the frontend and backend.

```bash
alectryon --frontend coqdoc coqdoc.v
alectryon --frontend coqdoc --backend webpage coqdoc.v -o coqdoc.html
```

--------------------------------

### Compile Coq to HTML from File

Source: https://github.com/cpitclaudel/alectryon/blob/main/recipes/tests/plain_cli.rst

Compiles a Coq file to an HTML webpage using Alectryon. The output is redirected to 'plain_cli.noext.html' after sanitizing temporary file names.

```bash
$ TMP=$(mktemp --tmpdir alectryon-XXXXX-tmp); echo "Check nat." > $TMP; \
    python -m "alectryon" --no-header --copy-assets none --frontend coq --backend webpage $TMP -o - | \
    sed 's/alectryon-.....-tmp/tmp/g' > plain_cli.noext.html
      # Coq → HTML; produces ‘plain_cli.noext.html’
```

--------------------------------

### Building Alectryon Output

Source: https://github.com/cpitclaudel/alectryon/blob/main/recipes/_output/tests/goal_names.v.html

Command to build Coq code into HTML using Alectryon.

```bash
alectryon --frontend coq goal_names.v # Coq → HTML; produces ‘goal_names.v.html’
```

--------------------------------

### Case-insensitive reference normalization

Source: https://github.com/cpitclaudel/alectryon/blob/main/recipes/_output/references.html

Demonstrates how reST normalizes block names for case-insensitive comparison, using 'Print eq.' as an example.

```Alectryon
Print eq.
```

--------------------------------

### Coq Command in reST Table (Intros)

Source: https://github.com/cpitclaudel/alectryon/blob/main/recipes/literate_reST.rst

Demonstrates nesting a Coq 'intros' command within a reStructuredText list-table for documentation purposes.

```coq
intros x y.
```

--------------------------------

### Embed Coq Code in HTML

Source: https://github.com/cpitclaudel/alectryon/blob/main/recipes/literate_HTML.html

Example of embedding Coq code within HTML <pre> tags for Alectryon processing.

```coq
Require Import ZArith.

Goal True /\ True.
  split. (* .unfold *)
  - exact I.

    Check nat. (* .unfold *)
  - exact I.
Qed.
```

--------------------------------

### Coq Goal with Nested Let Bindings

Source: https://github.com/cpitclaudel/alectryon/blob/main/recipes/sphinx/_build/html/corner_cases.html

Illustrates complex let-binding structures within a Coq goal and proof.

```coq
Goal let a := (let bb := let b := 1 in (b , b)%nat in
              let tt := let t := nat in (t * t)%type in
              bb <: tt) in
     fst a = snd a.

Proof.
  intros.
  reflexivity.
Qed.
```

--------------------------------

### Coq Proof with Minification

Source: https://github.com/cpitclaudel/alectryon/blob/main/recipes/_output/tests/minification.v.html

A Coq proof demonstrating minification. This example defines a recursive tree structure and proves a property about it.

```coq
Require Import PeanoNat.
Section Redundant.
  Context (non_negative := Nat.le_0_l).
  Fixpoint tree (n: nat) :=
    match n with
    | 0 => forall m: nat, m >= 0
    | S n => tree n /\ tree n
    end.
  Goal tree 4.

    repeat split.

    all: simpl.

    all: intros.

    all: idtac.

    1: {

1 apply non_negative. }

    1: {1b apply non_negative. }

    1: {1b apply non_negative. }

    1: {1b apply non_negative. }

    1: {1b apply non_negative. }

    1: {1b apply non_negative. }

    1: {1b apply non_negative. }

    1: {1b apply non_negative. }

    1: {1b apply non_negative. }

    1: {1b apply non_negative. }

    1: {1b apply non_negative. }

    1: {1b apply non_negative. }

    1: {1b apply non_negative. }
  Qed.
End Redundant.
```

--------------------------------

### Coq Definition with Literate Comments

Source: https://github.com/cpitclaudel/alectryon/blob/main/recipes/_output/tests/comments_in_definition.v.rst

Example of a Coq definition for 'is_zero' function, showing inline comments for base cases.

```coq
    Definition is_zero (n: Nat): bool :=
      match n with
      | O =>

Base case…

          true
      | Succ _ =>

… and another base case

          false
      end.
  End Example1.
```

--------------------------------

### Simple Proof with Exact Intro

Source: https://github.com/cpitclaudel/alectryon/blob/main/recipes/_output/tests/corner_cases.lean3.html

A concise proof of a tautology using `exact true.intro`.

```lean
example : true := by

> * * *
> 
> true exact true.intro
```

--------------------------------

### Proof Attempt with Destruct (Fails)

Source: https://github.com/cpitclaudel/alectryon/blob/main/recipes/_output/literate_coq.min.stdin.rst

A subsequent attempt to prove evenness correctness by destructing 'n', which also gets stuck.

```coq
destruct n.
      + (* n 
         split; inversion 1.
      + (* n 

Stuck again!
```