Coq Syntax Highlighting Test

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.
This entry was posted in Coq, Tools and tagged , , . Bookmark the permalink.

Leave a Reply

Your email address will not be published. Required fields are marked *

This site uses Akismet to reduce spam. Learn how your comment data is processed.