12345678910111213141516171819202122232425262728293031323334353637 |
- (set natArityFn (lambda (b Bool) ((Bool-ind Unit Empty) b)))
- ;; Typ Bólowski bo są dwa konstuktory - Zero i Następnik (aksjomatyke Peano).
- ;; Typ Jednostkowy i Pusty bo Zero nie przyjmuje argumentów a następnik przyjmuje jeden
- (set Nat (W natArityFn)) ; typ liczb naturalnych
- (set zero (WSup Nat false (lambda (e Empty) ((Empty-ind Nat) e)))) ; Typ pusty bo zero nie przyjmuje argumentów
- (set succ (lambda (n Nat) (WSup Nat true (lambda (u Unit) n)))) ; Typ jednostkowy bo następnik ma jeden argument
- (set double
- (W-rec
- (lambda (n Nat) Nat)
- (lambda (a Bool)
- ((Bool-rec
- (lambda (bl Bool)
- (Pi
- (f (Pi (ba (natArityFn bl)) Nat))
- (Pi
- (g (Pi (ba (natArityFn bl)) Nat))
- Nat)))
- (lambda (unitToNat0 (Pi (u Unit) Nat))
- (lambda (unitToNat1 (Pi (u Unit) Nat))
- (succ (succ (unitToNat1 tt)))))
- (lambda (eToNat0 (Pi (e Empty) Nat))
- (lambda (eToNat2 (Pi (e Empty) Nat))
- zero)))
- a))))
- (set zero-xD (double zero))
- (set one (succ zero))
- (set two (succ one))
- (set four (double two))
- (set four-xD (succ (succ two)))
- (set four-eq-four (Id four four-xD) (refl four)) ; dowód że 4 = 4
- (set four-eq-four-xD (Id four four-xD) (refl four-xD))
- double
|