| 123456789101112131415161718192021222324252627282930313233343536 |
- -- Proof irrelevance is nice when you want to work with subsets.
- module Subset where
- data True : Prop where
- tt : True
- data False : Prop where
- data (|) (A:Set)(P:A -> Prop) : Set where
- sub : (x:A) -> P x -> A | P
- data Nat : Set where
- zero : Nat
- suc : Nat -> Nat
- mutual
- IsEven : Nat -> Prop
- IsEven zero = True
- IsEven (suc n) = IsOdd n
- IsOdd : Nat -> Prop
- IsOdd zero = False
- IsOdd (suc n) = IsEven n
- Even : Set
- Even = Nat | IsEven
- Odd : Set
- Odd = Nat | IsOdd
- (+) : Nat -> Nat -> Nat
- zero + m = m
- suc n + m = suc (n + m)
|
