summaryrefslogtreecommitdiff
path: root/src/main.rs (follow)
Commit message (Collapse)AuthorAgeFilesLines
* some isabelle/hol verificationHEADmainstuebinm2024-06-291-24/+19
| | | | | | | | doesn't do much, just proves that the find function won't cause an error. also removes all uses of rust traits, since these are currently broken on the aeneas side.
* feat: make `find` extractableRaito Bezarius2024-04-181-1/+1
| | | | | | I was not borrowing `&self`! Signed-off-by: Raito Bezarius <masterancpp@gmail.com>
* feat: add `find` functionRaito Bezarius2024-04-161-0/+13
| | | | Signed-off-by: Raito Bezarius <masterancpp@gmail.com>
* feat: note on extraction for inductiveRaito Bezarius2024-04-121-0/+2
| | | | Signed-off-by: Raito Bezarius <masterancpp@gmail.com>
* Initial extractionRaito Bezarius2024-03-251-9/+7
| | | | Signed-off-by: Raito Bezarius <masterancpp@gmail.com>
* Initial commitRaito Bezarius2024-03-251-0/+61
Signed-off-by: Raito Bezarius <masterancpp@gmail.com>
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-22 20:23:39 +0000