Commit 2022-04-20 10:38 a3a166bc

View on Github →

chore(model_theory/encoding): Improve the encoding of terms (#13532) Makes it so that the encoding of terms no longer requires the assumption inhabited (L.term A). Adjusts following lemmas to use the encoding API more directly.

Estimated changes

Modified src/model_theory/encoding.lean

modified theorem first_order.language.term.card_le

modified def first_order.language.term.list_decode

modified theorem first_order.language.term.list_decode_encode_list

Modified src/model_theory/substructures.lean