Commit 2022-03-16 21:17 b24372f6

feat(model_theory/basic, terms_and_formulas): Helper functions for constant symbols (#12722) Defines a function language.con from A to constants of the language L[[A]]. Changes the coercion of a constant to a term to a function language.constants.term. Proves simp lemmas for interpretation of constant symbols and realization of constant terms.