Skip to content

Commit d53fb36

Browse files
authored
Merge pull request #93 from thomas-lamiaux/patch-1
Update 1_03_rocq_docs.md with new tuto foe equations
2 parents b796290 + 06cfb2d commit d53fb36

File tree

1 file changed

+5
-1
lines changed

1 file changed

+5
-1
lines changed

data/tutorials/platform/1_03_rocq_docs.md

+5-1
Original file line numberDiff line numberDiff line change
@@ -27,4 +27,8 @@ function and its associated elimination principle.
2727
- Equations and Well-founded Recursion [interactive
2828
version](https://coq.inria.fr/platform-docs/Tutorial_Equations_wf.html)
2929
and [source
30-
code](https://coq.inria.fr/platform-docs/Tutorial_Equations_wf.v)
30+
code](https://coq.inria.fr/platform-docs/Tutorial_Equations_wf.v)
31+
- Equations and Indexed inductive types, and tactics [interactive
32+
version](https://coq.inria.fr/platform-docs/Tutorial_Equations_indexed.html)
33+
and [source
34+
code](https://coq.inria.fr/platform-docs/Tutorial_Equations_indexed.v)

0 commit comments

Comments
 (0)