blob: cd82dd3502b353331026c82990dc14789ae5feae (
plain)
1
2
3
4
5
6
7
8
9
10
11
|
# Formalization notes
- Inhabited is not synthesized systematically for any type.
- Synthesize type aliases (?): requires to obtain this information before MIR.
## Bundle of specifications
Most of the time, we have naked types which does not exhibit their "expected" specification,
e.g. an `Ord` trait which does not prove that it's an order.
Ideally, we need to be able to build trait specifications and find a way to unbundle them and use them in the different tactics.
|
