diff options
| author | Georges Gonthier | 2019-03-25 12:44:41 +0100 |
|---|---|---|
| committer | Cyril Cohen | 2019-04-01 17:42:37 +0200 |
| commit | 8a62590dd06803fca626f429271f9ad578f06a96 (patch) | |
| tree | df754a00d245b2f3c9639bad6e3694ff563d2720 /mathcomp/character | |
| parent | c2c3ceae8a2eabed33028bfff306c5664d0b42f2 (diff) | |
Expand sample use as container in Inductive
Clarified that the sample use provided is an example rather than a
misplaced unit test.
Added the definition of generic recursors to the examples, for both
non-dependent and dependent use cases.
Diffstat (limited to 'mathcomp/character')
0 files changed, 0 insertions, 0 deletions