diff --git a/test-harness/src/snapshots/toolchain__attributes into-fstar.snap b/test-harness/src/snapshots/toolchain__attributes into-fstar.snap index 03baa5eff..16d6a4594 100644 --- a/test-harness/src/snapshots/toolchain__attributes into-fstar.snap +++ b/test-harness/src/snapshots/toolchain__attributes into-fstar.snap @@ -114,6 +114,18 @@ unfold instance impl: Core.Ops.Arith.t_Sub t_Int t_Int = unfold let add x y = x + y ''' +"Attributes.Issue_1266_.fst" = ''' +module Attributes.Issue_1266_ +#set-options "--fuel 0 --ifuel 1 --z3rlimit 15" +open Core +open FStar.Mul + +class t_T (v_Self: Type0) = { + f_v_pre:v_Self -> Type0; + f_v_post:x: v_Self -> x_future: v_Self -> pred: Type0{pred ==> true}; + f_v:x0: v_Self -> Prims.Pure v_Self (f_v_pre x0) (fun result -> f_v_post x0 result) +} +''' "Attributes.Nested_refinement_elim.fst" = ''' module Attributes.Nested_refinement_elim #set-options "--fuel 0 --ifuel 1 --z3rlimit 15" diff --git a/tests/Cargo.lock b/tests/Cargo.lock index 1a2c1f3b8..6a5d037af 100644 --- a/tests/Cargo.lock +++ b/tests/Cargo.lock @@ -320,7 +320,7 @@ checksum = "8a9ee70c43aaf417c914396645a0fa852624801b24ebb7ae78fe8272889ac888" [[package]] name = "hax-lib" -version = "0.1.0-rc.1" +version = "0.1.0" dependencies = [ "hax-lib-macros", "num-bigint", @@ -329,7 +329,7 @@ dependencies = [ [[package]] name = "hax-lib-macros" -version = "0.1.0-rc.1" +version = "0.1.0" dependencies = [ "hax-lib-macros-types", "paste", @@ -341,7 +341,7 @@ dependencies = [ [[package]] name = "hax-lib-macros-types" -version = "0.1.0-rc.1" +version = "0.1.0" dependencies = [ "proc-macro2", "quote", @@ -352,14 +352,14 @@ dependencies = [ [[package]] name = "hax-lib-protocol" -version = "0.1.0-rc.1" +version = "0.1.0" dependencies = [ "libcrux", ] [[package]] name = "hax-lib-protocol-macros" -version = "0.1.0-rc.1" +version = "0.1.0" dependencies = [ "proc-macro-error", "proc-macro2", diff --git a/tests/attributes/src/lib.rs b/tests/attributes/src/lib.rs index c0deae940..eb520f6a7 100644 --- a/tests/attributes/src/lib.rs +++ b/tests/attributes/src/lib.rs @@ -381,3 +381,11 @@ mod requires_mut { } } } + +mod issue_1266 { + #[hax_lib::attributes] + trait T { + #[hax_lib::ensures(|_|true)] + fn v(x: &mut Self); + } +}