#lang pie (claim list1 (List Nat)) (define list1 (:: 1 (:: 2 (:: 3 nil)))) (claim list2 (List Nat)) (define list2 (:: 4 (:: 5 (:: 6 nil)))) (claim list3 (List Atom)) (define list3 (:: 'eleeins (:: 'elezwei (:: 'eledrei nil)))) (claim list4 (List Atom)) (define list4 (:: 'elevier (:: 'elefünf (:: 'elesechs nil)))) (claim append ;(append Nat list1 list2) -> für listen mit listen zusammenfügen / (append Atom list3 list4) (Pi ((E U)) (-> (List E) (List E) (List E)))) (define append (lambda (E start end) (rec-List start end (lambda (e es rec) (:: e rec))))) (claim snoc ;(snoc Nat list1 4) -> für listen mit Nat zusammenfügen / (snoc Atom list3 'pie) (Pi ((E U)) (-> (List E) E (List E)))) (define snoc (lambda (E list end) (rec-List list (:: end nil) (lambda (e es rec) (:: e rec))))) (claim concat (Pi ((E U)) (-> (List E)(List E) (List E)))) (claim step-concat (Pi((E U )) (-> E (List E) (List E) (List E)))) (define step-concat (lambda(E) (lambda(e es concat) (snoc E concat e)))) (define concat ;(concat Nat list1 list2) dabei wird hintere liste immer umgedreht (lambda(E) (lambda(start end) (rec-List end start (step-concat E))))) (claim reverse (Pi ((E U)) (-> (List E) (List E)))) (claim step-reverse (Pi((E U )) (-> E (List E) (List E) (List E)))) (define step-reverse (lambda(E) (lambda(e es reverse) (snoc E reverse e)))) (define reverse ;(reverse Nat list1) (lambda(E) (lambda(es) (rec-List es (the(List E)nil) (step-reverse E))))) (claim correct-concat (Pi ((E U)) (-> (List E)(List E) (List E)))) (define correct-concat (lambda (E start end) (concat E start (reverse E end)))) (claim map (Pi ((A U) (B U)) (-> (-> A B) (List A) (List B)))) (define map ;(map Nat Nat (lambda(y)(add1 y)) list1) (lambda (A B f l) (rec-List l (the (List B) nil) (lambda (e es rec) (:: (f e) rec))))) (claim vec1 (Vec Nat 3)) (define vec1 (vec:: 1 (vec:: 2 (vec:: 3 vecnil)))) (claim vec2 (Vec Nat 4)) (define vec2 (vec:: 4 (vec:: 3 (vec:: 2 (vec:: 1 vecnil))))) (claim first ;(first Nat 2 vec1) / (first Nat 3 vec2) (Pi ((E U) (l Nat)) (-> (Vec E (add1 l)) E))) (define first (lambda (E l) (lambda (vec) (head vec)))) (claim rest ;(rest Nat 2 vec1) / (rest Nat 3 vec2) (Pi ((E U) (l Nat)) (-> (Vec E (add1 l)) (Vec E l)))) (define rest (lambda (E l) (lambda (vec) (tail vec)))) (claim + (-> Nat Nat Nat)) (define + (lambda (x y)(iter-Nat x y (lambda (a) (add1 a))))) (claim sub1 (-> Nat Nat)) (define sub1 (lambda (a) (rec-Nat a 0 (lambda (n-1 akk) n-1)))) (claim - (-> Nat Nat Nat)) (define - (lambda (x y) (iter-Nat y x (lambda (a) (sub1 a))))) (claim first-nats ;(first-nats 5) (Pi ((n Nat)) (Vec Nat n))) (define first-nats (lambda (n) (ind-Nat n (lambda (x) (Vec Nat x)) vecnil (lambda (n-1 first_n-1) (vec:: (add1 n-1) first_n-1))))) (claim count-from ;(count-from 1 10) von 1 zehn drauf (Pi ((start Nat) (n Nat)) (Vec Nat n))) (define count-from (lambda (start n) (ind-Nat n (lambda (x) (Vec Nat x)) vecnil (lambda (n-1 rec) (vec:: (sub1 (- (+ start n) n-1)) rec))))) (claim also-rec-Nat (Pi ((X U)) (-> Nat X (-> Nat X X) X))) (define also-rec-Nat ; k ist dim wird also ignoriert (lambda (X) (lambda (target base step) (ind-Nat target (lambda (k) X) base step))))