curry-howard

Slides of a (very) informal lecture of mine on the Curry-Howard correspondence

git clone: git://git.pablopie.xyz/curry-howard
Log
Files
Refs
README
LICENSE

Commit: d059a165a8966d210fd5c9adf45a5336edf66322
Parent: 3eae4e81033f022b54edea724fad87787e7b21c2
Author: Pablo <pablo-escobar@riseup.net>
Date: Sun, 9 Oct 2022 01:33:31 +0000

Minor change in some examples

Diffstat

2 files changed, 3 insertions, 5 deletions

Status	File Name	N° Changes	Insertions	Deletions
Modified	examples/example.lean	6	3	3
Modified	examples/hacker.txt	2	0	2

diff --git a/examples/example.lean b/examples/example.lean
@@ -1,9 +1,9 @@
-theorem ex : Or p q -> Or q p := by 
+lemma ex : Or p q → Or q p := by
   intro h
   match h with
-  | Or.inl _  => 
+  | Or.inl _  =>
     apply Or.inr
     assumption
-  | Or.inr h2 => 
+  | Or.inr h2 =>
     apply Or.inl
     exact h2

diff --git a/examples/hacker.txt b/examples/hacker.txt
@@ -11,5 +11,3 @@
 11011110010011011110001100010101110110100100100000
 10110010101101110111101110100101111011001111001111
 10100001010100010010111100001010011000010110111110
-10011100111000010001011101010110101110001100000010
-11011001001001110001000110110000110000111101110111