Library LangAlg.tools
Library LangAlg.language
Library LangAlg.finite_functions
Library LangAlg.graph
- Main definitions
- Graphs with decidable labels and vertices
- Boolean path predicate
- Morphisms between graphs with decidable vertices
Library LangAlg.sp_terms
Library LangAlg.sp_terms_graphs
- Definitions and basic facts
- From axiomatic containment to graph ordering
- From graph ordering to axiomatic containment
- Main result
Library LangAlg.w_terms
Library LangAlg.w_terms_graphs
Library LangAlg.terms
- Definitions
- General properties
- Variables and size
- Properties of ⟨_⟩
- Mirror of a term
- Language interpretation
Library LangAlg.terms_w_terms
Library LangAlg.terms_graphs
Library LangAlg.expr
- Main definitions
- Some elementary properties of this algebra
- Sum of a list of elements
- Normalisation of expressions
- Language interpretation
Library LangAlg.expr_terms
Library LangAlg.expr_graphs
Library LangAlg.to_lang_witness
Library LangAlg.completeness
Library LangAlg.algebra
This page has been generated by coqdoc