Library Cantor.rpo.rpo
- Module Type Precedence,
- Definition of a precedence.
- Module Type RPO,
- Definition of RPO from a precedence on symbols.
- Definition of rpo.
- rpo is a preorder, and its reflexive closure is an ordering.
- Main theorem: when the precedence is well-founded, so is the rpo.
- RPO is compatible with the instanciation by a substitution.
- RPO is compatible with adding context.
- Definition of size-based well-founded orderings for induction.
- Definition of rpo.
- rpo is a preorder, and its reflexive closure is an ordering.
- Well-foundedness of rpo.
- Main theorem: when the precedence is well-founded, so is the rpo.
- RPO is compatible with the instanciation by a substitution.
- RPO is compatible with adding context.
Library Cantor.rpo.term
- Term algebra defined as functor from a Module Signature and a Module Variable.
- Module Type Signature.
- Module Type Variables.
- Module Type Term built from a signature and a set of variables.
- A functor building a Term Module from a Signature and a set of Variables.
Library Cantor.misc.G4
Library Cantor.prelude.more_list
- Some additional properties for the Coq lists.