Commit 2022-03-05 16:13 51adf3a1

View on Github →

feat(model_theory/terms_and_formulas): Using a list encoding, bounds the number of terms (#12276) Defines term.list_encode and term.list_decode, which turn terms into lists, and reads off lists as lists of terms. Bounds the number of terms by the number of allowed symbols + omega.

Estimated changes

Modified src/model_theory/terms_and_formulas.lean

added theorem first_order.language.term.card_le

added def first_order.language.term.list_decode

added theorem first_order.language.term.list_decode_encode_list

added def first_order.language.term.list_encode

added theorem first_order.language.term.list_encode_injective