diff options
| -rw-r--r-- | PROBLEMES | 7 | ||||
| -rw-r--r-- | TODO | 1 |
2 files changed, 1 insertions, 7 deletions
@@ -1,10 +1,3 @@ -- Problème affichage de Cases (alpha-conversion dans les patterns) -====================================================================== -Inductive t : Set := c : nat->nat->t. -Definition foo' := [x:t]Cases x of (c y z) => (plus y z) end. -Print foo'. -====================================================================== - Des CASTEDCOMMAND s'affiche dans les scripts de preuves. Probleme d'affichage des scripts de preuve (disparition des THEN) @@ -52,3 +52,4 @@ Doc: - Suggestions de la formation Dans le Intros pattern on pourrait interpreter les _ comme des hypotheses sur lesquelles on ferait Clear immediatement +-> FAIT, semble-t'il
\ No newline at end of file |