mathlib3
98bd247d - feat(model_theory/types): Realized types (#17848)

Commit
3 years ago
feat(model_theory/types): Realized types (#17848) Defines `first_order.language.Theory.type_of`, the type of a given tuple. Defines what it means for a type to be realized. Co-authored-by: Aaron Anderson <65780815+awainverse@users.noreply.github.com>
Author
Parents
Loading