Commit 2022-04-29 20:31 90bd6f54
View on Github →feat(model_theory/encoding): A bound on the number of bounded formulas (#13616)
Gives an encoding first_order.language.bounded_formula.encoding of bounded formulas as lists.
Uses the encoding to bound the number of bounded formulas with first_order.language.bounded_formula.card_le.