diff --git a/talks/2024-grads/Demo.agda b/talks/2024-grads/Demo.agda index 02d32a5..69d7361 100644 --- a/talks/2024-grads/Demo.agda +++ b/talks/2024-grads/Demo.agda @@ -10,3 +10,15 @@ open import Data.Bool open import Data.Bool.Properties open ≡-Reasoning +isEven : ℕ → Bool +isEven zero = true +isEven (suc n) = not (isEven n) + +example : isEven 5 ≡ false +example = refl + +e+e≡e : ∀ (m n : ℕ) → isEven m ≡ true → isEven n ≡ true → isEven (m + n) ≡ true +e+e≡e zero n m-even n-even = n-even +e+e≡e (2+ m) n m-even n-even = + let IH = e+e≡e m n (trans (sym (not-involutive (isEven m))) m-even) n-even in + trans (not-involutive (isEven (m + n))) IH \ No newline at end of file diff --git a/talks/2024-grads/main.tex b/talks/2024-grads/main.tex index d01a5bf..1be8535 100644 --- a/talks/2024-grads/main.tex +++ b/talks/2024-grads/main.tex @@ -1,4 +1,4 @@ -\documentclass[a4paper]{beamer} +\documentclass[handout,a4paper]{beamer} \useoutertheme{miniframes} % \usetheme{Darmstadt} @@ -13,7 +13,7 @@ \nocite{*} % \setbeamercovered{transparent} -\setbeameroption{show notes on second screen=right} +% \setbeameroption{show notes on second screen=right} \title{Formalizing mathematics with cubical type theory} \author{Michael Zhang}