finished playing with abels tutorial

Dep.agda

@@ -4,6 +4,8 @@ data Nat : Set where
   zero : Nat
   suc  : Nat → Nat
 
+one = suc zero
+
 data L (A : Set) : Set where
   []   : L A
   _::_ : A → L A → L A
@@ -27,4 +29,74 @@ 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
 
+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
+
+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
+
+Proposition = Set
+
+data Absurd : Proposition where
+
+data Truth  : Proposition where
+  t : Truth
+
+data _∧_ (A B : Proposition) : Proposition where
+  and : A → B → A ∧ B
+
+fst : {A B : Proposition} → A ∧ B → A
+fst (and a b) = a
+
+snd : {A B : Proposition} → A ∧ B → B
+snd (and a b) = b
+
+_×_ = _∧_
+
+data _∨_ (A B : Proposition) : Proposition where
+  inl : A → A ∨ B
+  inr : B → A ∨ B
+
+case : {A B C : Proposition} → A ∨ B → (A → C) → (B → C) → C
+case (inl a) f g = f a
+case (inr b) f g = g b
+
+lemma : {A : Proposition} → A → A ∧ Truth
+lemma a = (and a t)
+
+comm∧ : {A B : Proposition} → A ∧ B → B ∧ A
+comm∧ (and a b) = (and b a)
+
+True : Bool → Proposition
+True true = Truth
+True false = Absurd
+
+refl≤ : (n : Nat) → True (n ≤ n)
+refl≤ zero    = t
+refl≤ (suc n) = refl≤ n
+
+data SList : Nat → Set where
+  snil  : SList zero
+  scons : {n : Nat}  (m : Nat) → True (n ≤ m) → SList n → SList m
+
+slist1 = scons one t (scons zero t snil)