Commit 26f51c58 authored by Raphael Cauderlier's avatar Raphael Cauderlier

Fix a typo

parent c059a9d6
......@@ -117,8 +117,8 @@ def eqv (p : prop) (q : prop) := and (imp p q) (imp q p).
def nand_list : props -> prop.
[] nand_list nil_prop --> true
[A] nand_list (cons_prop A nil_prop) --> A
[A1,A2,As] nand_list (cons_prop A1 (cons_prop A2 nil_prop))
--> and A1 (nand_list (cons_prop A2 nil_prop)).
[A1,A2,As] nand_list (cons_prop A1 (cons_prop A2 As))
--> and A1 (nand_list (cons_prop A2 As)).
(; nand_type n == propⁿ -> prop ;)
def nand_type : nat -> Type.
......@@ -136,8 +136,8 @@ def nand : n : nat -> nand_type n := nand_aux nil_prop.
def nor_list : props -> prop.
[] nor_list nil_prop --> false
[A] nor_list (cons_prop A nil_prop) --> A
[A1,A2,As] nor_list (cons_prop A1 (cons_prop A2 nil_prop))
--> or A1 (nor_list (cons_prop A2 nil_prop)).
[A1,A2,As] nor_list (cons_prop A1 (cons_prop A2 As))
--> or A1 (nor_list (cons_prop A2 As)).
def nor_aux : props -> n : nat -> nand_type n.
[Bs] nor_aux Bs nat.O --> nor_list Bs
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment