abstractions

cryspen · Feb 14, 2025 · a2c4c47 · a2c4c47
1 parent 442a269
commit a2c4c47
Show file tree

Hide file tree

Showing 2 changed files with 8 additions and 5 deletions.
diff --git a/hax-lib/proofs/fstar/extraction/Hax_lib.Abstraction.fst b/hax-lib/proofs/fstar/extraction/Hax_lib.Abstraction.fst
@@ -6,7 +6,3 @@ class t_Abstraction (v_Self: Type0) = {
       f_lift: v_Self -> f_AbstractType;
 }
 
-instance int_abs t : t_Abstraction (int_t t) {
-      f_AbstractType = int;
-      f_lift = fun x -> v x;
-}
diff --git a/hax-lib/proofs/fstar/extraction/Hax_lib.Int.fst b/hax-lib/proofs/fstar/extraction/Hax_lib.Int.fst
@@ -1,9 +1,16 @@
 module Hax_lib.Int
-
 open Core
+open Hax_lib.Abstraction
 
 unfold type t_Int = int
 
+instance int_abs t : t_Abstraction (int_t t) {
+      f_AbstractType = int;
+      f_lift = fun x -> v x;
+}
+
+let f_to_int = f_lift
+
 unfold let impl__Int__to_u8 (#t:inttype) (n:range_t t) : int_t t = mk_int #t n
 unfold let impl__Int__to_u16 (#t:inttype) (n:range_t t) : int_t t = mk_int #t n
 unfold let impl__Int__to_u32 (#t:inttype) (n:range_t t) : int_t t = mk_int #t n