From 37e8a0f5ff7d964eb9525fef765b38e44f79302b Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Fri, 24 May 2024 15:48:27 +0200 Subject: Update test outputs --- tests/fstar/traits/Traits.fst | 166 +++++++++++++++++++++--------------------- 1 file changed, 83 insertions(+), 83 deletions(-) (limited to 'tests/fstar/traits') diff --git a/tests/fstar/traits/Traits.fst b/tests/fstar/traits/Traits.fst index fa841e8a..70c345ba 100644 --- a/tests/fstar/traits/Traits.fst +++ b/tests/fstar/traits/Traits.fst @@ -6,20 +6,20 @@ open Primitives #set-options "--z3rlimit 50 --fuel 1 --ifuel 1" (** Trait declaration: [traits::BoolTrait] - Source: 'tests/src/traits.rs', lines 1:0-1:19 *) + Source: 'tests/src/traits.rs', lines 2:0-2:19 *) noeq type boolTrait_t (self : Type0) = { get_bool : self -> result bool; } (** [traits::{(traits::BoolTrait for bool)}::get_bool]: - Source: 'tests/src/traits.rs', lines 12:4-12:30 *) + Source: 'tests/src/traits.rs', lines 13:4-13:30 *) let boolTraitBool_get_bool (self : bool) : result bool = Ok self (** Trait implementation: [traits::{(traits::BoolTrait for bool)}] - Source: 'tests/src/traits.rs', lines 11:0-11:23 *) + Source: 'tests/src/traits.rs', lines 12:0-12:23 *) let boolTraitBool : boolTrait_t bool = { get_bool = boolTraitBool_get_bool; } (** [traits::BoolTrait::ret_true]: - Source: 'tests/src/traits.rs', lines 6:4-6:30 *) + Source: 'tests/src/traits.rs', lines 7:4-7:30 *) let boolTrait_ret_true (#self : Type0) (self_clause : boolTrait_t self) (self1 : self) : result bool @@ -27,49 +27,49 @@ let boolTrait_ret_true Ok true (** [traits::test_bool_trait_bool]: - Source: 'tests/src/traits.rs', lines 17:0-17:44 *) + Source: 'tests/src/traits.rs', lines 18:0-18:44 *) let test_bool_trait_bool (x : bool) : result bool = let* b = boolTraitBool_get_bool x in if b then boolTrait_ret_true boolTraitBool x else Ok false (** [traits::{(traits::BoolTrait for core::option::Option)#1}::get_bool]: - Source: 'tests/src/traits.rs', lines 23:4-23:30 *) + Source: 'tests/src/traits.rs', lines 24:4-24:30 *) let boolTraitOption_get_bool (t : Type0) (self : option t) : result bool = begin match self with | None -> Ok false | Some _ -> Ok true end (** Trait implementation: [traits::{(traits::BoolTrait for core::option::Option)#1}] - Source: 'tests/src/traits.rs', lines 22:0-22:31 *) + Source: 'tests/src/traits.rs', lines 23:0-23:31 *) let boolTraitOption (t : Type0) : boolTrait_t (option t) = { get_bool = boolTraitOption_get_bool t; } (** [traits::test_bool_trait_option]: - Source: 'tests/src/traits.rs', lines 31:0-31:54 *) + Source: 'tests/src/traits.rs', lines 32:0-32:54 *) let test_bool_trait_option (t : Type0) (x : option t) : result bool = let* b = boolTraitOption_get_bool t x in if b then boolTrait_ret_true (boolTraitOption t) x else Ok false (** [traits::test_bool_trait]: - Source: 'tests/src/traits.rs', lines 35:0-35:50 *) + Source: 'tests/src/traits.rs', lines 36:0-36:50 *) let test_bool_trait (t : Type0) (boolTraitInst : boolTrait_t t) (x : t) : result bool = boolTraitInst.get_bool x (** Trait declaration: [traits::ToU64] - Source: 'tests/src/traits.rs', lines 39:0-39:15 *) + Source: 'tests/src/traits.rs', lines 40:0-40:15 *) noeq type toU64_t (self : Type0) = { to_u64 : self -> result u64; } (** [traits::{(traits::ToU64 for u64)#2}::to_u64]: - Source: 'tests/src/traits.rs', lines 44:4-44:26 *) + Source: 'tests/src/traits.rs', lines 45:4-45:26 *) let toU64U64_to_u64 (self : u64) : result u64 = Ok self (** Trait implementation: [traits::{(traits::ToU64 for u64)#2}] - Source: 'tests/src/traits.rs', lines 43:0-43:18 *) + Source: 'tests/src/traits.rs', lines 44:0-44:18 *) let toU64U64 : toU64_t u64 = { to_u64 = toU64U64_to_u64; } (** [traits::{(traits::ToU64 for (A, A))#3}::to_u64]: - Source: 'tests/src/traits.rs', lines 50:4-50:26 *) + Source: 'tests/src/traits.rs', lines 51:4-51:26 *) let toU64Pair_to_u64 (a : Type0) (toU64Inst : toU64_t a) (self : (a & a)) : result u64 = let (x, x1) = self in @@ -78,75 +78,75 @@ let toU64Pair_to_u64 u64_add i i1 (** Trait implementation: [traits::{(traits::ToU64 for (A, A))#3}] - Source: 'tests/src/traits.rs', lines 49:0-49:31 *) + Source: 'tests/src/traits.rs', lines 50:0-50:31 *) let toU64Pair (a : Type0) (toU64Inst : toU64_t a) : toU64_t (a & a) = { to_u64 = toU64Pair_to_u64 a toU64Inst; } (** [traits::f]: - Source: 'tests/src/traits.rs', lines 55:0-55:36 *) + Source: 'tests/src/traits.rs', lines 56:0-56:36 *) let f (t : Type0) (toU64Inst : toU64_t t) (x : (t & t)) : result u64 = toU64Pair_to_u64 t toU64Inst x (** [traits::g]: - Source: 'tests/src/traits.rs', lines 59:0-61:18 *) + Source: 'tests/src/traits.rs', lines 60:0-62:18 *) let g (t : Type0) (toU64PairInst : toU64_t (t & t)) (x : (t & t)) : result u64 = toU64PairInst.to_u64 x (** [traits::h0]: - Source: 'tests/src/traits.rs', lines 66:0-66:24 *) + Source: 'tests/src/traits.rs', lines 67:0-67:24 *) let h0 (x : u64) : result u64 = toU64U64_to_u64 x (** [traits::Wrapper] - Source: 'tests/src/traits.rs', lines 70:0-70:21 *) + Source: 'tests/src/traits.rs', lines 71:0-71:21 *) type wrapper_t (t : Type0) = { x : t; } (** [traits::{(traits::ToU64 for traits::Wrapper)#4}::to_u64]: - Source: 'tests/src/traits.rs', lines 75:4-75:26 *) + Source: 'tests/src/traits.rs', lines 76:4-76:26 *) let toU64traitsWrapper_to_u64 (t : Type0) (toU64Inst : toU64_t t) (self : wrapper_t t) : result u64 = toU64Inst.to_u64 self.x (** Trait implementation: [traits::{(traits::ToU64 for traits::Wrapper)#4}] - Source: 'tests/src/traits.rs', lines 74:0-74:35 *) + Source: 'tests/src/traits.rs', lines 75:0-75:35 *) let toU64traitsWrapper (t : Type0) (toU64Inst : toU64_t t) : toU64_t (wrapper_t t) = { to_u64 = toU64traitsWrapper_to_u64 t toU64Inst; } (** [traits::h1]: - Source: 'tests/src/traits.rs', lines 80:0-80:33 *) + Source: 'tests/src/traits.rs', lines 81:0-81:33 *) let h1 (x : wrapper_t u64) : result u64 = toU64traitsWrapper_to_u64 u64 toU64U64 x (** [traits::h2]: - Source: 'tests/src/traits.rs', lines 84:0-84:41 *) + Source: 'tests/src/traits.rs', lines 85:0-85:41 *) let h2 (t : Type0) (toU64Inst : toU64_t t) (x : wrapper_t t) : result u64 = toU64traitsWrapper_to_u64 t toU64Inst x (** Trait declaration: [traits::ToType] - Source: 'tests/src/traits.rs', lines 88:0-88:19 *) + Source: 'tests/src/traits.rs', lines 89:0-89:19 *) noeq type toType_t (self t : Type0) = { to_type : self -> result t; } (** [traits::{(traits::ToType for u64)#5}::to_type]: - Source: 'tests/src/traits.rs', lines 93:4-93:28 *) + Source: 'tests/src/traits.rs', lines 94:4-94:28 *) let toTypeU64Bool_to_type (self : u64) : result bool = Ok (self > 0) (** Trait implementation: [traits::{(traits::ToType for u64)#5}] - Source: 'tests/src/traits.rs', lines 92:0-92:25 *) + Source: 'tests/src/traits.rs', lines 93:0-93:25 *) let toTypeU64Bool : toType_t u64 bool = { to_type = toTypeU64Bool_to_type; } (** Trait declaration: [traits::OfType] - Source: 'tests/src/traits.rs', lines 98:0-98:16 *) + Source: 'tests/src/traits.rs', lines 99:0-99:16 *) noeq type ofType_t (self : Type0) = { of_type : (t : Type0) -> (toTypeInst : toType_t t self) -> t -> result self; } (** [traits::h3]: - Source: 'tests/src/traits.rs', lines 104:0-104:50 *) + Source: 'tests/src/traits.rs', lines 105:0-105:50 *) let h3 (t1 t2 : Type0) (ofTypeInst : ofType_t t1) (toTypeInst : toType_t t2 t1) (y : t2) : @@ -155,14 +155,14 @@ let h3 ofTypeInst.of_type t2 toTypeInst y (** Trait declaration: [traits::OfTypeBis] - Source: 'tests/src/traits.rs', lines 109:0-109:36 *) + Source: 'tests/src/traits.rs', lines 110:0-110:36 *) noeq type ofTypeBis_t (self t : Type0) = { toTypeInst : toType_t t self; of_type : t -> result self; } (** [traits::h4]: - Source: 'tests/src/traits.rs', lines 118:0-118:57 *) + Source: 'tests/src/traits.rs', lines 119:0-119:57 *) let h4 (t1 t2 : Type0) (ofTypeBisInst : ofTypeBis_t t1 t2) (toTypeInst : toType_t t2 t1) (y : t2) : @@ -171,34 +171,34 @@ let h4 ofTypeBisInst.of_type y (** [traits::TestType] - Source: 'tests/src/traits.rs', lines 122:0-122:22 *) + Source: 'tests/src/traits.rs', lines 123:0-123:22 *) type testType_t (t : Type0) = t (** [traits::{traits::TestType#6}::test::TestType1] - Source: 'tests/src/traits.rs', lines 127:8-127:24 *) + Source: 'tests/src/traits.rs', lines 128:8-128:24 *) type testType_test_TestType1_t = u64 (** Trait declaration: [traits::{traits::TestType#6}::test::TestTrait] - Source: 'tests/src/traits.rs', lines 128:8-128:23 *) + Source: 'tests/src/traits.rs', lines 129:8-129:23 *) noeq type testType_test_TestTrait_t (self : Type0) = { test : self -> result bool; } (** [traits::{traits::TestType#6}::test::{(traits::{traits::TestType#6}::test::TestTrait for traits::{traits::TestType#6}::test::TestType1)}::test]: - Source: 'tests/src/traits.rs', lines 139:12-139:34 *) + Source: 'tests/src/traits.rs', lines 140:12-140:34 *) let testType_test_TestTraittraitsTestTypetestTestType1_test (self : testType_test_TestType1_t) : result bool = Ok (self > 1) (** Trait implementation: [traits::{traits::TestType#6}::test::{(traits::{traits::TestType#6}::test::TestTrait for traits::{traits::TestType#6}::test::TestType1)}] - Source: 'tests/src/traits.rs', lines 138:8-138:36 *) + Source: 'tests/src/traits.rs', lines 139:8-139:36 *) let testType_test_TestTraittraitsTestTypetestTestType1 : testType_test_TestTrait_t testType_test_TestType1_t = { test = testType_test_TestTraittraitsTestTypetestTestType1_test; } (** [traits::{traits::TestType#6}::test]: - Source: 'tests/src/traits.rs', lines 126:4-126:36 *) + Source: 'tests/src/traits.rs', lines 127:4-127:36 *) let testType_test (t : Type0) (toU64Inst : toU64_t t) (self : testType_t t) (x : t) : result bool @@ -209,11 +209,11 @@ let testType_test else Ok false (** [traits::BoolWrapper] - Source: 'tests/src/traits.rs', lines 150:0-150:22 *) + Source: 'tests/src/traits.rs', lines 151:0-151:22 *) type boolWrapper_t = bool (** [traits::{(traits::ToType for traits::BoolWrapper)#7}::to_type]: - Source: 'tests/src/traits.rs', lines 156:4-156:25 *) + Source: 'tests/src/traits.rs', lines 157:4-157:25 *) let toTypetraitsBoolWrapperT_to_type (t : Type0) (toTypeBoolTInst : toType_t bool t) (self : boolWrapper_t) : result t @@ -221,14 +221,14 @@ let toTypetraitsBoolWrapperT_to_type toTypeBoolTInst.to_type self (** Trait implementation: [traits::{(traits::ToType for traits::BoolWrapper)#7}] - Source: 'tests/src/traits.rs', lines 152:0-152:33 *) + Source: 'tests/src/traits.rs', lines 153:0-153:33 *) let toTypetraitsBoolWrapperT (t : Type0) (toTypeBoolTInst : toType_t bool t) : toType_t boolWrapper_t t = { to_type = toTypetraitsBoolWrapperT_to_type t toTypeBoolTInst; } (** [traits::WithConstTy::LEN2] - Source: 'tests/src/traits.rs', lines 164:4-164:21 *) + Source: 'tests/src/traits.rs', lines 165:4-165:21 *) let with_const_ty_len2_default_body (self : Type0) (len : usize) : result usize = Ok 32 @@ -236,7 +236,7 @@ let with_const_ty_len2_default (self : Type0) (len : usize) : usize = eval_global (with_const_ty_len2_default_body self len) (** Trait declaration: [traits::WithConstTy] - Source: 'tests/src/traits.rs', lines 161:0-161:39 *) + Source: 'tests/src/traits.rs', lines 162:0-162:39 *) noeq type withConstTy_t (self : Type0) (len : usize) = { cLEN1 : usize; cLEN2 : usize; @@ -247,18 +247,18 @@ noeq type withConstTy_t (self : Type0) (len : usize) = { } (** [traits::{(traits::WithConstTy<32: usize> for bool)#8}::LEN1] - Source: 'tests/src/traits.rs', lines 175:4-175:21 *) + Source: 'tests/src/traits.rs', lines 176:4-176:21 *) let with_const_ty_bool32_len1_body : result usize = Ok 12 let with_const_ty_bool32_len1 : usize = eval_global with_const_ty_bool32_len1_body (** [traits::{(traits::WithConstTy<32: usize> for bool)#8}::f]: - Source: 'tests/src/traits.rs', lines 180:4-180:39 *) + Source: 'tests/src/traits.rs', lines 181:4-181:39 *) let withConstTyBool32_f (i : u64) (a : array u8 32) : result u64 = Ok i (** Trait implementation: [traits::{(traits::WithConstTy<32: usize> for bool)#8}] - Source: 'tests/src/traits.rs', lines 174:0-174:29 *) + Source: 'tests/src/traits.rs', lines 175:0-175:29 *) let withConstTyBool32 : withConstTy_t bool 32 = { cLEN1 = with_const_ty_bool32_len1; cLEN2 = with_const_ty_len2_default bool 32; @@ -269,7 +269,7 @@ let withConstTyBool32 : withConstTy_t bool 32 = { } (** [traits::use_with_const_ty1]: - Source: 'tests/src/traits.rs', lines 183:0-183:75 *) + Source: 'tests/src/traits.rs', lines 184:0-184:75 *) let use_with_const_ty1 (h : Type0) (len : usize) (withConstTyInst : withConstTy_t h len) : result usize @@ -277,7 +277,7 @@ let use_with_const_ty1 Ok withConstTyInst.cLEN1 (** [traits::use_with_const_ty2]: - Source: 'tests/src/traits.rs', lines 187:0-187:73 *) + Source: 'tests/src/traits.rs', lines 188:0-188:73 *) let use_with_const_ty2 (h : Type0) (len : usize) (withConstTyInst : withConstTy_t h len) (w : withConstTyInst.tW) : @@ -286,7 +286,7 @@ let use_with_const_ty2 Ok () (** [traits::use_with_const_ty3]: - Source: 'tests/src/traits.rs', lines 189:0-189:80 *) + Source: 'tests/src/traits.rs', lines 190:0-190:80 *) let use_with_const_ty3 (h : Type0) (len : usize) (withConstTyInst : withConstTy_t h len) (x : withConstTyInst.tW) : @@ -295,12 +295,12 @@ let use_with_const_ty3 withConstTyInst.tW_clause_0.to_u64 x (** [traits::test_where1]: - Source: 'tests/src/traits.rs', lines 193:0-193:40 *) + Source: 'tests/src/traits.rs', lines 194:0-194:40 *) let test_where1 (t : Type0) (_x : t) : result unit = Ok () (** [traits::test_where2]: - Source: 'tests/src/traits.rs', lines 194:0-194:57 *) + Source: 'tests/src/traits.rs', lines 195:0-195:57 *) let test_where2 (t : Type0) (withConstTyT32Inst : withConstTy_t t 32) (_x : u32) : result unit @@ -308,7 +308,7 @@ let test_where2 Ok () (** Trait declaration: [traits::ParentTrait0] - Source: 'tests/src/traits.rs', lines 200:0-200:22 *) + Source: 'tests/src/traits.rs', lines 201:0-201:22 *) noeq type parentTrait0_t (self : Type0) = { tW : Type0; get_name : self -> result string; @@ -316,24 +316,24 @@ noeq type parentTrait0_t (self : Type0) = { } (** Trait declaration: [traits::ParentTrait1] - Source: 'tests/src/traits.rs', lines 205:0-205:22 *) + Source: 'tests/src/traits.rs', lines 206:0-206:22 *) type parentTrait1_t (self : Type0) = unit (** Trait declaration: [traits::ChildTrait] - Source: 'tests/src/traits.rs', lines 206:0-206:49 *) + Source: 'tests/src/traits.rs', lines 207:0-207:49 *) noeq type childTrait_t (self : Type0) = { parentTrait0Inst : parentTrait0_t self; parentTrait1Inst : parentTrait1_t self; } (** [traits::test_child_trait1]: - Source: 'tests/src/traits.rs', lines 209:0-209:56 *) + Source: 'tests/src/traits.rs', lines 210:0-210:56 *) let test_child_trait1 (t : Type0) (childTraitInst : childTrait_t t) (x : t) : result string = childTraitInst.parentTrait0Inst.get_name x (** [traits::test_child_trait2]: - Source: 'tests/src/traits.rs', lines 213:0-213:54 *) + Source: 'tests/src/traits.rs', lines 214:0-214:54 *) let test_child_trait2 (t : Type0) (childTraitInst : childTrait_t t) (x : t) : result childTraitInst.parentTrait0Inst.tW @@ -341,7 +341,7 @@ let test_child_trait2 childTraitInst.parentTrait0Inst.get_w x (** [traits::order1]: - Source: 'tests/src/traits.rs', lines 219:0-219:59 *) + Source: 'tests/src/traits.rs', lines 220:0-220:59 *) let order1 (t u : Type0) (parentTrait0Inst : parentTrait0_t t) (parentTrait0Inst1 : parentTrait0_t u) : @@ -350,27 +350,27 @@ let order1 Ok () (** Trait declaration: [traits::ChildTrait1] - Source: 'tests/src/traits.rs', lines 222:0-222:35 *) + Source: 'tests/src/traits.rs', lines 223:0-223:35 *) noeq type childTrait1_t (self : Type0) = { parentTrait1Inst : parentTrait1_t self; } (** Trait implementation: [traits::{(traits::ParentTrait1 for usize)#9}] - Source: 'tests/src/traits.rs', lines 224:0-224:27 *) + Source: 'tests/src/traits.rs', lines 225:0-225:27 *) let parentTrait1Usize : parentTrait1_t usize = () (** Trait implementation: [traits::{(traits::ChildTrait1 for usize)#10}] - Source: 'tests/src/traits.rs', lines 225:0-225:26 *) + Source: 'tests/src/traits.rs', lines 226:0-226:26 *) let childTrait1Usize : childTrait1_t usize = { parentTrait1Inst = parentTrait1Usize; } (** Trait declaration: [traits::Iterator] - Source: 'tests/src/traits.rs', lines 229:0-229:18 *) + Source: 'tests/src/traits.rs', lines 230:0-230:18 *) noeq type iterator_t (self : Type0) = { tItem : Type0; } (** Trait declaration: [traits::IntoIterator] - Source: 'tests/src/traits.rs', lines 233:0-233:22 *) + Source: 'tests/src/traits.rs', lines 234:0-234:22 *) noeq type intoIterator_t (self : Type0) = { tItem : Type0; tIntoIter : Type0; @@ -379,107 +379,107 @@ noeq type intoIterator_t (self : Type0) = { } (** Trait declaration: [traits::FromResidual] - Source: 'tests/src/traits.rs', lines 250:0-250:21 *) + Source: 'tests/src/traits.rs', lines 251:0-251:21 *) type fromResidual_t (self t : Type0) = unit (** Trait declaration: [traits::Try] - Source: 'tests/src/traits.rs', lines 246:0-246:48 *) + Source: 'tests/src/traits.rs', lines 247:0-247:48 *) noeq type try_t (self : Type0) = { tResidual : Type0; fromResidualSelftraitsTryResidualInst : fromResidual_t self tResidual; } (** Trait declaration: [traits::WithTarget] - Source: 'tests/src/traits.rs', lines 252:0-252:20 *) + Source: 'tests/src/traits.rs', lines 253:0-253:20 *) noeq type withTarget_t (self : Type0) = { tTarget : Type0; } (** Trait declaration: [traits::ParentTrait2] - Source: 'tests/src/traits.rs', lines 256:0-256:22 *) + Source: 'tests/src/traits.rs', lines 257:0-257:22 *) noeq type parentTrait2_t (self : Type0) = { tU : Type0; tU_clause_0 : withTarget_t tU; } (** Trait declaration: [traits::ChildTrait2] - Source: 'tests/src/traits.rs', lines 260:0-260:35 *) + Source: 'tests/src/traits.rs', lines 261:0-261:35 *) noeq type childTrait2_t (self : Type0) = { parentTrait2Inst : parentTrait2_t self; convert : parentTrait2Inst.tU -> result parentTrait2Inst.tU_clause_0.tTarget; } (** Trait implementation: [traits::{(traits::WithTarget for u32)#11}] - Source: 'tests/src/traits.rs', lines 264:0-264:23 *) + Source: 'tests/src/traits.rs', lines 265:0-265:23 *) let withTargetU32 : withTarget_t u32 = { tTarget = u32; } (** Trait implementation: [traits::{(traits::ParentTrait2 for u32)#12}] - Source: 'tests/src/traits.rs', lines 268:0-268:25 *) + Source: 'tests/src/traits.rs', lines 269:0-269:25 *) let parentTrait2U32 : parentTrait2_t u32 = { tU = u32; tU_clause_0 = withTargetU32; } (** [traits::{(traits::ChildTrait2 for u32)#13}::convert]: - Source: 'tests/src/traits.rs', lines 273:4-273:29 *) + Source: 'tests/src/traits.rs', lines 274:4-274:29 *) let childTrait2U32_convert (x : u32) : result u32 = Ok x (** Trait implementation: [traits::{(traits::ChildTrait2 for u32)#13}] - Source: 'tests/src/traits.rs', lines 272:0-272:24 *) + Source: 'tests/src/traits.rs', lines 273:0-273:24 *) let childTrait2U32 : childTrait2_t u32 = { parentTrait2Inst = parentTrait2U32; convert = childTrait2U32_convert; } (** Trait declaration: [traits::CFnOnce] - Source: 'tests/src/traits.rs', lines 286:0-286:23 *) + Source: 'tests/src/traits.rs', lines 287:0-287:23 *) noeq type cFnOnce_t (self args : Type0) = { tOutput : Type0; call_once : self -> args -> result tOutput; } (** Trait declaration: [traits::CFnMut] - Source: 'tests/src/traits.rs', lines 292:0-292:37 *) + Source: 'tests/src/traits.rs', lines 293:0-293:37 *) noeq type cFnMut_t (self args : Type0) = { cFnOnceInst : cFnOnce_t self args; call_mut : self -> args -> result (cFnOnceInst.tOutput & self); } (** Trait declaration: [traits::CFn] - Source: 'tests/src/traits.rs', lines 296:0-296:33 *) + Source: 'tests/src/traits.rs', lines 297:0-297:33 *) noeq type cFn_t (self args : Type0) = { cFnMutInst : cFnMut_t self args; call : self -> args -> result cFnMutInst.cFnOnceInst.tOutput; } (** Trait declaration: [traits::GetTrait] - Source: 'tests/src/traits.rs', lines 300:0-300:18 *) + Source: 'tests/src/traits.rs', lines 301:0-301:18 *) noeq type getTrait_t (self : Type0) = { tW : Type0; get_w : self -> result tW; } (** [traits::test_get_trait]: - Source: 'tests/src/traits.rs', lines 305:0-305:49 *) + Source: 'tests/src/traits.rs', lines 306:0-306:49 *) let test_get_trait (t : Type0) (getTraitInst : getTrait_t t) (x : t) : result getTraitInst.tW = getTraitInst.get_w x (** Trait declaration: [traits::Trait] - Source: 'tests/src/traits.rs', lines 310:0-310:15 *) + Source: 'tests/src/traits.rs', lines 311:0-311:15 *) noeq type trait_t (self : Type0) = { cLEN : usize; } (** [traits::{(traits::Trait for @Array)#14}::LEN] - Source: 'tests/src/traits.rs', lines 315:4-315:20 *) + Source: 'tests/src/traits.rs', lines 316:4-316:20 *) let trait_array_len_body (t : Type0) (n : usize) : result usize = Ok n let trait_array_len (t : Type0) (n : usize) : usize = eval_global (trait_array_len_body t n) (** Trait implementation: [traits::{(traits::Trait for @Array)#14}] - Source: 'tests/src/traits.rs', lines 314:0-314:40 *) + Source: 'tests/src/traits.rs', lines 315:0-315:40 *) let traitArray (t : Type0) (n : usize) : trait_t (array t n) = { cLEN = trait_array_len t n; } (** [traits::{(traits::Trait for traits::Wrapper)#15}::LEN] - Source: 'tests/src/traits.rs', lines 319:4-319:20 *) + Source: 'tests/src/traits.rs', lines 320:4-320:20 *) let traittraits_wrapper_len_body (t : Type0) (traitInst : trait_t t) : result usize = Ok 0 @@ -487,19 +487,19 @@ let traittraits_wrapper_len (t : Type0) (traitInst : trait_t t) : usize = eval_global (traittraits_wrapper_len_body t traitInst) (** Trait implementation: [traits::{(traits::Trait for traits::Wrapper)#15}] - Source: 'tests/src/traits.rs', lines 318:0-318:35 *) + Source: 'tests/src/traits.rs', lines 319:0-319:35 *) let traittraitsWrapper (t : Type0) (traitInst : trait_t t) : trait_t (wrapper_t t) = { cLEN = traittraits_wrapper_len t traitInst; } (** [traits::use_wrapper_len]: - Source: 'tests/src/traits.rs', lines 322:0-322:43 *) + Source: 'tests/src/traits.rs', lines 323:0-323:43 *) let use_wrapper_len (t : Type0) (traitInst : trait_t t) : result usize = Ok (traittraitsWrapper t traitInst).cLEN (** [traits::Foo] - Source: 'tests/src/traits.rs', lines 326:0-326:20 *) + Source: 'tests/src/traits.rs', lines 327:0-327:20 *) type foo_t (t u : Type0) = { x : t; y : u; } (** [core::result::Result] @@ -510,7 +510,7 @@ type core_result_Result_t (t e : Type0) = | Core_result_Result_Err : e -> core_result_Result_t t e (** [traits::{traits::Foo#16}::FOO] - Source: 'tests/src/traits.rs', lines 332:4-332:33 *) + Source: 'tests/src/traits.rs', lines 333:4-333:33 *) let foo_foo_body (t u : Type0) (traitInst : trait_t t) : result (core_result_Result_t t i32) = Ok (Core_result_Result_Err 0) @@ -519,13 +519,13 @@ let foo_foo (t u : Type0) (traitInst : trait_t t) eval_global (foo_foo_body t u traitInst) (** [traits::use_foo1]: - Source: 'tests/src/traits.rs', lines 335:0-335:48 *) + Source: 'tests/src/traits.rs', lines 336:0-336:48 *) let use_foo1 (t u : Type0) (traitInst : trait_t t) : result (core_result_Result_t t i32) = Ok (foo_foo t u traitInst) (** [traits::use_foo2]: - Source: 'tests/src/traits.rs', lines 339:0-339:48 *) + Source: 'tests/src/traits.rs', lines 340:0-340:48 *) let use_foo2 (t u : Type0) (traitInst : trait_t u) : result (core_result_Result_t u i32) = Ok (foo_foo u t traitInst) -- cgit v1.2.3