Skip to content
GitLab
Menu
Projects
Groups
Snippets
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
Pierre Letouzey
prog-lmfi
Commits
5b71def4
Commit
5b71def4
authored
Oct 29, 2019
by
Pierre Letouzey
Browse files
TD1: un peu plus de booléen
parent
b65f1321
Changes
1
Hide whitespace changes
Inline
Side-by-side
td1.md
View file @
5b71def4
...
...
@@ -69,6 +69,8 @@ Définir également deux fonctions `nat2church : nat -> church` et `church2nat :
-
Tester si
`fun a b c => a || b || c || negb (a && b) || negb (a && c)`
est une tautologie.
NB: la commande
`Open Scope bool_scope.`
permet de disposer des notations
`||`
et
`&&`
(en lieu et place de
`orb`
et
`andb`
)
-
Définir des fonctions se comportant comme
`negb`
,
`orb`
,
`andb`
du système.
#### Exercice 5 : fonctions usuelles sur les entiers
Définir les fonctions suivantes sur le type
`nat`
(sans utiliser celles fournies par le système):
...
...
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment