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)

1 files changed, 6 insertions, 0 deletions

diff --git a/compiler/Main.ml b/compiler/Main.ml
index d78b9081..ff6a4d67 100644
--- a/compiler/Main.ml
+++ b/compiler/Main.ml
@@ -253,6 +253,12 @@ let () =
             (* We don't support fuel for the HOL4 backend *)
             if !use_fuel then (
               log#error "The HOL4 backend doesn't support the -use-fuel option";
+              fail ())
+        | IsabelleHOL ->
+            record_fields_short_names := true;
+            (* We don't support fuel for the IsabelleHOL backend *)
+            if !use_fuel then (
+              log#error "The IsabelleHOL backend doesn't support the -use-fuel option";
               fail ()))
   in