abstractions

cryspen · Feb 14, 2025 · b234531 · b234531
1 parent a2c4c47
commit b234531
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/hax-lib/proofs/fstar/extraction/Hax_lib.Int.fst b/hax-lib/proofs/fstar/extraction/Hax_lib.Int.fst
@@ -9,7 +9,7 @@ instance int_abs t : t_Abstraction (int_t t) {
       f_lift = fun x -> v x;
 }
 
-let f_to_int = f_lift
+unfold 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