From 5e35e3875884ca4be63f253d9e8d7f2fc71b3527 Mon Sep 17 00:00:00 2001 From: Raito Bezarius Date: Thu, 28 Mar 2024 17:59:35 +0100 Subject: 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 --- notes.md | 11 +++++++++++ 1 file changed, 11 insertions(+) create mode 100644 notes.md (limited to 'notes.md') 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. -- cgit v1.2.3