summaryrefslogtreecommitdiff
path: root/doc/tutorial/arithm/Arithm.gf
blob: 00d6b478074f2d46982a766ed9a6d9814b57366b (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
abstract Arithm = {

  cat
    Prop ;
    Nat ;

  fun
    Zero : Nat ;
    Succ : Nat -> Nat ;
    Even : Nat -> Prop ;
    And  : Prop -> Prop -> Prop ;

}