Mysaa/m1-internship
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

added examples

Browse Source
This commit is contained in:
Thorsten Altenkirch 2023-06-20 15:36:18 +02:00
parent bd99520e35
commit 309ba6ab70
1 changed files with 5 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

5
fol.agda
View File

@ -77,5 +77,10 @@ example {A = A} = lam (lam (App (app (suc zero)
(wk-subst {A = A}) (App zero zero))) zero))
-- (∀ x ∀ y . A(x,y)) ⇒ ∀ y ∀ x . A(y,x)
-- (A ⇒ ∀ x . B(x)) ⇒ ∀ x . A ⇒ B(x)
-- ∀ x y . A(x,y) ⇒ ∀ x . A(x,x)
-- ∀ x . A (x) ⇒ ∀ x y . A(x)
-- (((∀ x . A (x)) ⇒ B)⇒ B) ⇒ ∀ x . ((A (x) ⇒ B) ⇒ B)
-}