Completed adequacy (adeq) proof for naturals.

gebn · Feb 20, 2015 · 9d9a7e7 · 9d9a7e7
1 parent 08d6fa4
commit 9d9a7e7
Showing 1 changed file with 2 additions and 1 deletion.
diff --git a/Proofs/Adequacy.agda b/Proofs/Adequacy.agda
@@ -25,7 +25,8 @@ adeq : (T : Set) (e : Exp T) (p : Program) (σ : State) (n : ℕ) →
 adeq .𝔹 (B _) _ _ _ () -- nothing ≡ just n is false
 
 -- naturals
-adeq .ℕ (N x) p σ n eq = {!!}
+adeq .ℕ (N .zero) p σ zero refl = suc zero , refl    -- just zero is trivially equal to just (zero ∷ [])
+adeq .ℕ (N .(suc n)) p σ (suc n) refl = suc n , refl -- just (suc n) is trivially equal to just (suc n ∷ [])
 
 -- variables
 adeq .ℕ (V x) p σ n eq = {!!}