A test case for Coq syntax highlighting in GeSHi (for the WP-Syntax plugin).

Inductive nat : Set := | O : nat | S : nat -> nat. Inductive fin : nat -> Type := | FO : forall n, fin (S n) | FS : forall n, fin n -> fin (S n). Implicit Arguments FO [n]. Implicit Arguments FS [n]. Fixpoint fin2nat {n : nat} (k : fin n) : nat := match k with | FO _ => 0 | FS _ k' => S (fin2nat k') end. Example f0 : fin 3 := FO. Example f1 : fin 3 := FS FO. Example f2 : fin 3 := FS (FS FO). Eval compute in fin2nat f2. |