Library test

This is the first documentation.

First section

Require ZArith.

First sub-section

Second sub-section

First sub-sub-section toto

First sub-sub-sub-section.

Definition of function f:

Definition f [x:nat] : nat := Cases x of O => O | (S p) => p end.

The same on multiple lines with indentation

Definition g [x:nat] : nat :=
  Cases x of
    | O => O
    | (S p) => p
  end.

Implicits g [1 2 3].


Pwd.

Here is a Coq term: [x:nat]x and some formatted piece of Coq

Definition h :=
      Cases O of _ => (S O) end

and the remaining of the documentation...

Features tests

Lists

Here is a list: first item (1) first sub-item (1.1) second sub-item (1.2) second item (2) first sub-item (2.1) first sub-sub-item (2.1.1)

Rule

Verbatim

Here is the corresponding caml code: let rec fact n = if n <= 1 then 1 else n * fact (n-1)

Escapings

Escaping to Latex maths:

Escaping to Latex:

Escaping to HTML: home ∀

Gallina tests




this is a doc with quotation x:nat

Lemma l2: (A:Prop)A->A.
Intro.
Auto.
Save.

Goal (A:Prop)A->A.
Auto.
Save l3.

Theorem l4: (A:Prop)A->A.
Auto.
Qed.

Fact l5: (A:Prop)A->A.
Idtac; Idtac. Exact l3. Defined.

Theorem foo: (a:Prop) a->~~a.
Qed.

Local l4 : (A:Set)A->A.
Intros A x. Exact x.
Defined.

Pretty-printing tests

balanced square brackets within escaped Coq: {A}+{B} and a following comment...

printing / remove printing of symbol ->~

->~

-->

∀

->~

x [+I*] y

UTF-8 symbols

∀

∀

test in escape ∀ x:nat. x=x

greek letters

α

α

letter-like

Ä

Ä

notations with square brackets

x [#] y

x [#] y

and within a comment x [#] y is correctly parsed and nicely written...

x {-} y

x {-} y

and within a comment x {-} y is correctly parsed and nicely written...

Sections and modules

Module M.

Import A.

Module Type N.

End N.

Section S.

Definition t := Type.

End S.

End M.

Tests about identifier toto

Tests about identifier toto

Comments

bla bla bla (Peano.plus x y) toto 3