diff options
| author | Erik Martin-Dorel | 2019-08-07 00:47:03 +0200 |
|---|---|---|
| committer | Erik Martin-Dorel | 2019-08-08 11:11:52 +0200 |
| commit | 05ae4be1258ed198949f886e83151fb41f7dedb1 (patch) | |
| tree | b19ec4e61b98ec789287afc3c9b7352731456024 /kernel/cPrimitives.ml | |
| parent | d60b807c868f4d54a273549519ea51c196242370 (diff) | |
[ssr] under: Add a contrived example to test under/over with Setoids
* Borrow ideas from the Setoid refman documentation:
https://coq.inria.fr/refman/addendum/generalized-rewriting.html#first-class-setoids-and-morphisms
* Introduce a relation with the following signature:
[Rel : forall (m n : nat) (s : Setoid m n), car s -> car s -> Prop]
Diffstat (limited to 'kernel/cPrimitives.ml')
0 files changed, 0 insertions, 0 deletions