Skip to content

Commit

Permalink
Tutorial about Intro patterns (#73)
Browse files Browse the repository at this point in the history
* 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]>
  • Loading branch information
4 people authored Jan 3, 2025
1 parent e786299 commit ee8f08b
Show file tree
Hide file tree
Showing 2 changed files with 549 additions and 0 deletions.
Loading

0 comments on commit ee8f08b

Please sign in to comment.