|
| Coq |
Agda |
Twelf |
| Usage |
$ nano myprog.v
$ coqtop
Coq < Load myprog.
Coq < Quit.
|
$ nano myprog.agda
$ agda myprog.agda
|
$ nano myprog.elf
$ twelf/bin/twelf-server
loadFile myprog.elf
quit
|
| Comments |
(* This is a comment *)
|
{- This is a comment -}
-- This is a comment
|
% This is a comment
|
Conventions |
|
|
constant, Variable |
| Types |
Type |
Set |
kind, type, term |
| Natural numbers |
nat, O, S |
Nat, zero, suc |
nat, zero, suc |
| Function types |
A -> B
(x:A) : B
(x:A) (y:B) : C
|
A -> B
(x:A) -> B
(x:A) -> (y:B) -> C
|
A -> B
{x:A} B
|
| Anonymous function |
fun x:T => y |
\(x:T) => y |
[x:T] y |
| Recursive type |
Inductive ord : Type :=
| zero : ord
| suc : ord -> ord
| lim : (nat -> ord) -> ord.
|
data Ord : Set where
zo : Ord
so : Ord -> Ord
lo : (Nat -> Ord) -> Ord
|
ord : type.
zero : ord.
suc : ord -> ord.
lim : (nat -> ord) -> ord.
|
| Simple definitions |
Definition a := b.
Definition a (x:T) : U := b.
|
a : b
|
a = b.
|
| Recursive definition |
Fixpoint plus (n:nat) (m:nat) : nat :=
match n with
| O => m
| S p => S (plus p m)
end.
|
plus : (n:nat) -> (m:nat) -> Nat
plus 0 m = m
plus (suc p) m = suc (plus p m)
|
plus : nat -> nat -> nat -> type.
pz : plus zero Y Y.
ps : plus (suc X) Y (suc Z)
<- plus X Y Z.
|
| Theorem |
Theorem plus_O_n :
forall n:nat, O + n = n.
proof.
intros n. reflexivity.
Qed.
|
forall {n:Nat} -> zero + n = n
|
%theorem
plus0n : forall {N:nat}
plus 0 N N.
|
| Polymorphism |
Definition id : (a:Type) : a -> a :=
fun (x:a) => x.
|
id : (A: Set) -> A -> A
id A x = x
or
id = \(A:Set) -> \(x:A) x
or
id : {A:Set} -> A -> A
id x = x
|
No polymorphism |