Commit 2022-03-31 16:09 13e08bf3

feat(model_theory/*): Constructors for low-arity languages and structures (#12960) Defines first_order.language.mk₂ to make it easier to define a language with at-most-binary symbols. Defines first_order.language.Structure.mk₂ to make it easier to define a structure in a language defined with first_order.language₂. Defines first_order.language.functions.apply₁ and first_order.language.functions.apply₂ to make it easier to construct terms using low-arity function symbols. Defines first_order.language.relations.formula₁ and first_order.language.relations.formula₂ to make it easier to construct formulas using low-arity relation symbols.