Commit e6a4c2ce authored by Pierre Letouzey's avatar Pierre Letouzey
Browse files

typos

parent 9ede9f16
......@@ -37,7 +37,7 @@ A dot `.` is mandatory to end each Coq phrase.
Define a function `compose : forall A B C, (B->C)->(A->B)->(A->C)`. Test it with functions `S` and `pred` on natural numbers (type `nat`).
#### Exercise 2 : boolean ersatz
#### Exercise 2 : Boolean ersatz
Define (without using `bool` nor any other inductive type):
......@@ -54,7 +54,7 @@ More precisely, define (without using `nat` nor any other inductive type):
- a type `church : Type`
- two constant `zero` and `one` of type `church`
- a function `succ` of type `church->church`
- two fonctions `plus` and `mult` of type `church->church->church`
- two functions `plus` and `mult` of type `church->church->church`
- a function `power`
- a test `iszero`
......@@ -62,16 +62,16 @@ Also define two functions `nat2church : nat -> church` and `church2nat : church
## Base types
#### Exercise 4 : booleans
#### Exercise 4 : Booleans
- Write a function `checktauto : (bool->bool)->bool` which tests whether a boolean unary function always answers `true`.
- Write a function `checktauto : (bool->bool)->bool` which tests whether a Boolean unary function always answers `true`.
- Same for `checktauto2` et `checktauto3` for boolean fonctions expecting 2, then 3 arguments. This can be done by enumerating all cases, but there is a clever way to proceed (for instance by re-using `checktauto`.
- Same for `checktauto2` and `checktauto3` for Boolean functions expecting 2, then 3 arguments. This can be done by enumerating all cases, but there is a clever way to proceed (for instance by re-using `checktauto`.
- Check wether `fun a b c => a || b || c || negb (a && b) || negb (a && c)` is a tautology.
- Check whether `fun a b c => a || b || c || negb (a && b) || negb (a && c)` is a tautology.
Note : the command `Open Scope bool_scope.` activates notations `||` and `&&` (respectively for functions `orb` and `andb`).
- Define some functions behavint like Coq standard functions `negb` and `orb` and `andb`.
- Define some functions behaving like Coq standard functions `negb` and `orb` and `andb`.
#### Exercise 5 : usual functions on natural numbers.
......
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