module DepTypesDemo where data Nat : Set where zero : Nat suc : Nat -> Nat infix 2 _+_ infix 3 _*_ _+_ : Nat -> Nat -> Nat n + zero = n n + suc m = suc (n + m) _*_ : Nat -> Nat -> Nat n * zero = zero n * (suc m) = n * m + n {- data Vect (A : Set) : Nat -> Set where vnil : Vect A zero vcons : (n : Nat) -> A -> Vect A n -> Vect A (suc n) inner : (n : Nat) -> Vect Nat n -> Vect Nat n -> Nat inner zero vnil vnil = zero inner (suc .n) (vcons .n x xs) (vcons n y ys) = x * y + inner n xs ys -} data Vect (A : Set) : Nat -> Set where vnil : Vect A zero vcons : {n : Nat} -> A -> Vect A n -> Vect A (suc n) inner : {n : Nat} -> Vect Nat n -> Vect Nat n -> Nat inner vnil vnil = zero inner (vcons x xs) (vcons y ys) = x * y + inner xs ys one = suc zero two = suc one v1 = vcons one vnil v2 = vcons zero v1 {- foo = inner v1 v2 -} append : {A : Set}{n m : Nat} -> Vect A n -> Vect A m -> Vect A (n + m) append vnil ys = ys append (vcons x xs) ys = vcons x (append xs ys) {- append : {A : Set}{n m : Nat} -> Vect A n -> Vect A m -> Vect A (m + n) append vnil ys = ys append (vcons x xs) ys = vcons x (append xs ys) -} data Fin : Nat -> Set where fzero : {n : Nat} -> Fin (suc n) fsuc : {n : Nat} -> Fin n -> Fin (suc n) _!!_ : {A : Set}{n : Nat} -> Vect A n -> Fin n -> A vnil !! () vcons x xs !! fzero = x vcons x xs !! fsuc m = xs !! m -- test = vnil !! fzero data Bool : Set where true : Bool false : Bool if_then_else_ : {A : Set} -> Bool -> A -> A -> A if true then b1 else b2 = b1 if false then b1 else b2 = b2 _≤_ : Nat -> Nat -> Bool zero ≤ n = true (suc m) ≤ zero = false (suc m) ≤ (suc n) = m ≤ n {- data SList : Nat -> Set where snil : SList zero scons : {n : Nat}(m : Nat) -> SList n -> (n ≤ m) -> SList m -} Proposition = Set data _&_ (A B : Proposition) : Proposition where _,_ : A -> B -> A & B fst : {A B : Proposition} -> A & B -> A fst (a , b) = a _×_ = _&_ data _||_ (A B : Proposition) : Proposition where inl : A -> A || B inr : B -> A || B data Truth : Proposition where tt : Truth data Absurd : Proposition where lemma : {A : Proposition} -> A -> A & Truth lemma a = (a , tt) comm& : {A B : Proposition} -> A & B -> B & A comm& (a , b) = (b , a) True : Bool -> Proposition True true = Truth True false = Absurd refl≤ : (n : Nat) -> True (n ≤ n) refl≤ zero = tt refl≤ (suc n) = refl≤ n bla : (n : Nat) -> True (one ≤ zero) bla n = bla (suc n) foo : True (one ≤ zero) -- foo = bla zero foo = foo A : Bool -> Proposition A true = Truth A false = True (one ≤ zero) {- prf : (b : Bool) -> A b prf true = tt bar : True (one ≤ zero) bar = prf false -} data SList : Nat -> Set where snil : SList zero scons : {n : Nat}(m : Nat) -> True (n ≤ m) -> SList n -> SList m slist1 = scons one tt (scons zero tt snil) slist2 = scons zero {! !} (scons one tt snil)