diff options
| author | Raito Bezarius | 2024-03-28 17:59:35 +0100 |
|---|---|---|
| committer | Raito Bezarius | 2024-03-28 20:30:56 +0100 |
| commit | 5e35e3875884ca4be63f253d9e8d7f2fc71b3527 (patch) | |
| tree | ce607fcdda121b87b133791d5e708c6809559a20 /notes.md | |
| parent | 33a92dac2635ead90cb84c16023355a7d679d434 (diff) | |
refactor: generalize the theory and perform some lifts
Move forward the "HSpec" idea, move around files, construct the hierarchy of trees, etc.
Signed-off-by: Raito Bezarius <masterancpp@gmail.com>
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. |