| Commit message (Collapse) | Author | Age | Files | Lines |
|
|
|
|
|
|
|
| |
After a complete 180 with the Order theory, we close the goals of find
and insert and we give an example of U32 order that we will upstream to
Aeneas directly.
Signed-off-by: Raito Bezarius <masterancpp@gmail.com>
|
|
|
|
| |
Signed-off-by: Raito Bezarius <masterancpp@gmail.com>
|
|
|
|
| |
Signed-off-by: Raito Bezarius <masterancpp@gmail.com>
|
|
|
|
|
|
| |
I was not borrowing `&self`!
Signed-off-by: Raito Bezarius <masterancpp@gmail.com>
|
|
|
|
|
|
| |
So that I stop doing `nix run` one-offs!
Signed-off-by: Raito Bezarius <masterancpp@gmail.com>
|
|
|
|
|
|
| |
Now, we speak only about equivalence.
Signed-off-by: Raito Bezarius <masterancpp@gmail.com>
|
|
|
|
|
|
|
| |
We revamp the typeclass mechanisms and we add an equality hypothesis
now.
Signed-off-by: Raito Bezarius <masterancpp@gmail.com>
|
|
|
|
| |
Signed-off-by: Raito Bezarius <masterancpp@gmail.com>
|
|
|
|
| |
Signed-off-by: Raito Bezarius <masterancpp@gmail.com>
|
|
|
|
| |
Signed-off-by: Raito Bezarius <masterancpp@gmail.com>
|
|
|
|
| |
Signed-off-by: Raito Bezarius <masterancpp@gmail.com>
|
| |
|
|
|
|
| |
Signed-off-by: Raito Bezarius <masterancpp@gmail.com>
|
|
|
|
| |
Signed-off-by: Raito Bezarius <masterancpp@gmail.com>
|
|
|
|
| |
Signed-off-by: Raito Bezarius <masterancpp@gmail.com>
|
|
|
|
| |
Signed-off-by: Raito Bezarius <masterancpp@gmail.com>
|
|\
| |
| | |
refactor: generalize the theory and perform some lifts
|
| |
| |
| |
| | |
Signed-off-by: Raito Bezarius <masterancpp@gmail.com>
|
| |
| |
| |
| | |
Signed-off-by: Raito Bezarius <masterancpp@gmail.com>
|
| |
| |
| |
| | |
Signed-off-by: Raito Bezarius <masterancpp@gmail.com>
|
| |
| |
| |
| | |
Signed-off-by: Raito Bezarius <masterancpp@gmail.com>
|
| |
| |
| |
| | |
Signed-off-by: Raito Bezarius <masterancpp@gmail.com>
|
|/
|
|
|
|
| |
Move forward the "HSpec" idea, move around files, construct the hierarchy of trees, etc.
Signed-off-by: Raito Bezarius <masterancpp@gmail.com>
|
|
|
|
|
|
| |
This is a first property which is generic of all BSTs.
Signed-off-by: Raito Bezarius <masterancpp@gmail.com>
|
|
|
|
| |
Signed-off-by: Raito Bezarius <masterancpp@gmail.com>
|
|
Signed-off-by: Raito Bezarius <masterancpp@gmail.com>
|