Commit 2022-04-29 17:28 8360f2c8
View on Github →feat(model_theory/language_map, bundled): Reducts of structures (#13745)
Defines first_order.language.Lhom.reduct which pulls a structure back along a language map.
Defines first_order.language.Theory.Model.reduct which sends a model of (φ.on_Theory T) to its reduct as a model of T.