diff options
Diffstat (limited to 'notes.md')
| -rw-r--r-- | notes.md | 11 |
1 files changed, 11 insertions, 0 deletions
diff --git a/notes.md b/notes.md new file mode 100644 index 0000000..cd82dd3 --- /dev/null +++ b/notes.md @@ -0,0 +1,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. |