diff options
| author |  sacerdot <sacerdot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-10-06 09:20:36 +0000 |
|---|---|---|
| committer | sacerdot <sacerdot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-10-06 09:20:36 +0000 |
| commit | 5777b87e11c187035b8784ff3dd95f90844de400 (patch) | |
| tree | f5d1e6c7d2399bdec64e56b2a6880a2dee1224a2 /CREDITS | |
| parent | dc3990966375ed617b175fa9a35f4bbe14b9d9ff (diff) | |
Leibniz equality is now a quantified relation.
This means that you can declare a morphism signature that has an argument
(or its output type) that is just eq.
E.g.:
Add Morphism incl with signature incl --> eq ++> impl.
is a correct signature for a morphism property of type
forall A, list A -> list A -> Prop
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6183 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'CREDITS')
0 files changed, 0 insertions, 0 deletions