Abstract Substitution (Q7361907)
From MaRDI portal
!
This is the item page for this Wikibase entity, intended for internal use and editing purposes. Please use the normal view instead:
AFP entry Abstract_Substitution
| Language | Label | Description | Also known as |
|---|---|---|---|
| default for all languages | No label defined |
||
| English | Abstract Substitution |
AFP entry Abstract_Substitution |
Statements
16 September 2024
0 references
Martin Desharnais-Schäfer
0 references
Balazs Toth
0 references
Abstract Substitution (English)
0 references
This entry provides a small, reusable, theory that specifies the abstract concept of substition as monoid action. Both the substitution type and the object type are kept abstract. The theory provides multiple useful definitions and lemmas. Two example usages are provided for first order terms: one for terms from the AFP/First_Order_Terms session and one for terms from the Isabelle/HOL-ex session.
0 references
