Commit ee8f08b
Tutorial about Intro patterns (#73)
* sec1
* write most of sec 3 and 4
* some work on section 5
* first draft
* first draft 2
* typo
* edit index
* Fix Pierre Courtieu's comments
* separate example of sec5 in two part => rewriting sec3 & views sec5
* Apply suggestions from code review
Co-authored-by: Quentin VERMANDE <[email protected]>
* add ex Exists
* Apply suggestions from code review
Co-authored-by: Pierre Rousselin <[email protected]>
* Apply suggestions from code review
* add Pierre Rousselin's example
* add parentheses
* add Lyes Saadi's comment
* Add other tactics with as
also correct some whitespace issues and add a small remark after the
first "destruct as".
* Update src/Tutorial_intro_patterns.v
---------
Co-authored-by: Quentin VERMANDE <[email protected]>
Co-authored-by: Pierre Rousselin <[email protected]>
Co-authored-by: Pierre Rousselin <[email protected]>1 parent e786299 commit ee8f08b
2 files changed
+549
-0
lines changed
0 commit comments