diff options
| author | stuebinm | 2024-06-29 21:31:22 +0200 |
|---|---|---|
| committer | stuebinm | 2024-06-29 22:11:04 +0200 |
| commit | 59214186b817329342d9d72e23adf12f7a3b1348 (patch) | |
| tree | 8292abe4ca52e9742f6a4ff9d102565a6362e665 /compiler/SymbolicToPure.ml | |
| parent | 5590dc87a5426cbcb32a2387701d179e107a9792 (diff) | |
had some fun writing an IsabelleHOL backend
(do not actually use this, most things are broken, and the primitives
lib barely exists and is simply incorrect. But it is enough to create
syntax-correct Isabelle code for relatively simply rust code, as long
as it does not contain any uses of traits)
Diffstat (limited to '')
| -rw-r--r-- | compiler/SymbolicToPure.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml index e829ed30..3f858124 100644 --- a/compiler/SymbolicToPure.ml +++ b/compiler/SymbolicToPure.ml @@ -3754,7 +3754,7 @@ let wrap_in_match_fuel (span : Meta.span) (fuel0 : VarId.id) (fuel : VarId.id) let match_ty = body.ty in let match_e = Switch (fuel0, Match [ fail_branch; success_branch ]) in { e = match_e; ty = match_ty } - | Lean | HOL4 -> + | Lean | HOL4 | IsabelleHOL -> (* We should have checked the command line arguments before *) raise (Failure "Unexpected") |