Tutorial about Intro patterns - #73

Merged

thomas-lamiaux merged 20 commits into

rocq-prover:mainfrom

thomas-lamiaux:intro-patterns

Jan 3, 2025

Commits on Dec 23, 2024

sec1
thomas-lamiaux
committed
cdcce00
write most of sec 3 and 4
thomas-lamiaux
committed
400f070
some work on section 5
thomas-lamiaux
committed
aeacd91
first draft
thomas-lamiaux
committed
acecc89
first draft 2
thomas-lamiaux
committed
96a78ba
typo
thomas-lamiaux
committed
e7ad5cb
edit index
thomas-lamiaux
committed
f1eb5fa

Commits on Dec 24, 2024

Commits on Dec 27, 2024

Apply suggestions from code review

thomas-lamiaux
and
Tragicus
authored
47df7aa

Commits on Dec 28, 2024

add ex Exists
thomas-lamiaux
committed
1b6e0df
Apply suggestions from code review

thomas-lamiaux
and
Villetaneuse
authored
c62193a
Apply suggestions from code review
thomas-lamiaux
authored
9e4774d
add Pierre Rousselin's example
thomas-lamiaux
committed
44286d8
add parentheses
thomas-lamiaux
committed
d89551e
add Lyes Saadi's comment
thomas-lamiaux
committed
0822b03

Commits on Dec 30, 2024

Add other tactics with as
Villetaneuse
committed
65bc16d

Commits on Jan 3, 2025