diff options
Diffstat (limited to '')
| -rw-r--r-- | tests/coq/traits/Traits.v | 50 |
1 files changed, 24 insertions, 26 deletions
diff --git a/tests/coq/traits/Traits.v b/tests/coq/traits/Traits.v index 0e942c7d..fb37a507 100644 --- a/tests/coq/traits/Traits.v +++ b/tests/coq/traits/Traits.v @@ -20,7 +20,7 @@ Arguments BoolTrait_t_get_bool { _ }. (** [traits::{(traits::BoolTrait for bool)}::get_bool]: Source: 'src/traits.rs', lines 12:4-12:30 *) Definition boolTraitBool_get_bool (self : bool) : result bool := - Return self. + Ok self. (** Trait implementation: [traits::{(traits::BoolTrait for bool)}] Source: 'src/traits.rs', lines 11:0-11:23 *) @@ -32,21 +32,21 @@ Definition BoolTraitBool : BoolTrait_t bool := {| Source: 'src/traits.rs', lines 6:4-6:30 *) Definition boolTrait_ret_true {Self : Type} (self_clause : BoolTrait_t Self) (self : Self) : result bool := - Return true + Ok true . (** [traits::test_bool_trait_bool]: Source: 'src/traits.rs', lines 17:0-17:44 *) Definition test_bool_trait_bool (x : bool) : result bool := b <- boolTraitBool_get_bool x; - if b then boolTrait_ret_true BoolTraitBool x else Return false + if b then boolTrait_ret_true BoolTraitBool x else Ok false . (** [traits::{(traits::BoolTrait for core::option::Option<T>)#1}::get_bool]: Source: 'src/traits.rs', lines 23:4-23:30 *) Definition boolTraitOption_get_bool (T : Type) (self : option T) : result bool := - match self with | None => Return false | Some _ => Return true end + match self with | None => Ok false | Some _ => Ok true end . (** Trait implementation: [traits::{(traits::BoolTrait for core::option::Option<T>)#1}] @@ -59,7 +59,7 @@ Definition BoolTraitOption (T : Type) : BoolTrait_t (option T) := {| Source: 'src/traits.rs', lines 31:0-31:54 *) Definition test_bool_trait_option (T : Type) (x : option T) : result bool := b <- boolTraitOption_get_bool T x; - if b then boolTrait_ret_true (BoolTraitOption T) x else Return false + if b then boolTrait_ret_true (BoolTraitOption T) x else Ok false . (** [traits::test_bool_trait]: @@ -81,7 +81,7 @@ Arguments ToU64_t_to_u64 { _ }. (** [traits::{(traits::ToU64 for u64)#2}::to_u64]: Source: 'src/traits.rs', lines 44:4-44:26 *) Definition toU64U64_to_u64 (self : u64) : result u64 := - Return self. + Ok self. (** Trait implementation: [traits::{(traits::ToU64 for u64)#2}] Source: 'src/traits.rs', lines 43:0-43:18 *) @@ -167,7 +167,7 @@ Arguments ToType_t_to_type { _ _ }. (** [traits::{(traits::ToType<bool> for u64)#5}::to_type]: Source: 'src/traits.rs', lines 93:4-93:28 *) Definition toTypeU64Bool_to_type (self : u64) : result bool := - Return (self s> 0%u64) + Ok (self s> 0%u64) . (** Trait implementation: [traits::{(traits::ToType<bool> for u64)#5}] @@ -238,7 +238,7 @@ Arguments TestType_test_TestTrait_t_test { _ }. Source: 'src/traits.rs', lines 139:12-139:34 *) Definition testType_test_TestTraittraitsTestTypetestTestType1_test (self : TestType_test_TestType1_t) : result bool := - Return (self s> 1%u64) + Ok (self s> 1%u64) . (** Trait implementation: [traits::{traits::TestType<T>#6}::test::{(traits::{traits::TestType<T>#6}::test::TestTrait for traits::{traits::TestType<T>#6}::test::TestType1)}] @@ -258,7 +258,7 @@ Definition testType_test x1 <- toU64Inst.(ToU64_t_to_u64) x; if x1 s> 0%u64 then testType_test_TestTraittraitsTestTypetestTestType1_test 0%u64 - else Return false + else Ok false . (** [traits::BoolWrapper] @@ -285,7 +285,7 @@ Definition ToTypetraitsBoolWrapperT (T : Type) (toTypeBoolTInst : ToType_t bool Source: 'src/traits.rs', lines 164:4-164:21 *) Definition with_const_ty_len2_default_body (Self : Type) (LEN : usize) : result usize := - Return 32%usize + Ok 32%usize . Definition with_const_ty_len2_default (Self : Type) (LEN : usize) : usize := (with_const_ty_len2_default_body Self LEN)%global @@ -313,7 +313,7 @@ Arguments WithConstTy_t_f { _ _ }. (** [traits::{(traits::WithConstTy<32: usize> for bool)#8}::LEN1] Source: 'src/traits.rs', lines 175:4-175:21 *) -Definition with_const_ty_bool32_len1_body : result usize := Return 12%usize. +Definition with_const_ty_bool32_len1_body : result usize := Ok 12%usize. Definition with_const_ty_bool32_len1 : usize := with_const_ty_bool32_len1_body%global . @@ -322,7 +322,7 @@ Definition with_const_ty_bool32_len1 : usize := Source: 'src/traits.rs', lines 180:4-180:39 *) Definition withConstTyBool32_f (i : u64) (a : array u8 32%usize) : result u64 := - Return i + Ok i . (** Trait implementation: [traits::{(traits::WithConstTy<32: usize> for bool)#8}] @@ -342,7 +342,7 @@ Definition use_with_const_ty1 (H : Type) (LEN : usize) (withConstTyInst : WithConstTy_t H LEN) : result usize := - Return withConstTyInst.(WithConstTy_tWithConstTy_t_LEN1) + Ok withConstTyInst.(WithConstTy_tWithConstTy_t_LEN1) . (** [traits::use_with_const_ty2]: @@ -352,7 +352,7 @@ Definition use_with_const_ty2 (w : withConstTyInst.(WithConstTy_tWithConstTy_t_W)) : result unit := - Return tt + Ok tt . (** [traits::use_with_const_ty3]: @@ -368,7 +368,7 @@ Definition use_with_const_ty3 (** [traits::test_where1]: Source: 'src/traits.rs', lines 193:0-193:40 *) Definition test_where1 (T : Type) (_x : T) : result unit := - Return tt. + Ok tt. (** [traits::test_where2]: Source: 'src/traits.rs', lines 194:0-194:57 *) @@ -376,7 +376,7 @@ Definition test_where2 (T : Type) (withConstTyT32Inst : WithConstTy_t T 32%usize) (_x : u32) : result unit := - Return tt + Ok tt . (** Trait declaration: [traits::ParentTrait0] @@ -435,7 +435,7 @@ Definition order1 ParentTrait0_t U) : result unit := - Return tt + Ok tt . (** Trait declaration: [traits::ChildTrait1] @@ -552,7 +552,7 @@ Definition ParentTrait2U32 : ParentTrait2_t u32 := {| (** [traits::{(traits::ChildTrait2 for u32)#13}::convert]: Source: 'src/traits.rs', lines 273:4-273:29 *) Definition childTrait2U32_convert (x : u32) : result u32 := - Return x. + Ok x. (** Trait implementation: [traits::{(traits::ChildTrait2 for u32)#13}] Source: 'src/traits.rs', lines 272:0-272:24 *) @@ -625,9 +625,7 @@ Arguments Trait_tTrait_t_LEN { _ }. (** [traits::{(traits::Trait for @Array<T, N>)#14}::LEN] Source: 'src/traits.rs', lines 315:4-315:20 *) -Definition trait_array_len_body (T : Type) (N : usize) : result usize := - Return N -. +Definition trait_array_len_body (T : Type) (N : usize) : result usize := Ok N. Definition trait_array_len (T : Type) (N : usize) : usize := (trait_array_len_body T N)%global . @@ -642,7 +640,7 @@ Definition TraitArray (T : Type) (N : usize) : Trait_t (array T N) := {| Source: 'src/traits.rs', lines 319:4-319:20 *) Definition traittraits_wrapper_len_body (T : Type) (traitInst : Trait_t T) : result usize := - Return 0%usize + Ok 0%usize . Definition traittraits_wrapper_len (T : Type) (traitInst : Trait_t T) : usize := @@ -659,7 +657,7 @@ Definition TraittraitsWrapper (T : Type) (traitInst : Trait_t T) : Trait_t (** [traits::use_wrapper_len]: Source: 'src/traits.rs', lines 322:0-322:43 *) Definition use_wrapper_len (T : Type) (traitInst : Trait_t T) : result usize := - Return (TraittraitsWrapper T traitInst).(Trait_tTrait_t_LEN) + Ok (TraittraitsWrapper T traitInst).(Trait_tTrait_t_LEN) . (** [traits::Foo] @@ -685,7 +683,7 @@ Arguments Core_result_Result_Err { _ _ }. Source: 'src/traits.rs', lines 332:4-332:33 *) Definition foo_foo_body (T U : Type) (traitInst : Trait_t T) : result (core_result_Result_t T i32) := - Return (Core_result_Result_Err 0%i32) + Ok (Core_result_Result_Err 0%i32) . Definition foo_foo (T U : Type) (traitInst : Trait_t T) : core_result_Result_t T i32 := @@ -696,14 +694,14 @@ Definition foo_foo (T U : Type) (traitInst : Trait_t T) Source: 'src/traits.rs', lines 335:0-335:48 *) Definition use_foo1 (T U : Type) (traitInst : Trait_t T) : result (core_result_Result_t T i32) := - Return (foo_foo T U traitInst) + Ok (foo_foo T U traitInst) . (** [traits::use_foo2]: Source: 'src/traits.rs', lines 339:0-339:48 *) Definition use_foo2 (T U : Type) (traitInst : Trait_t U) : result (core_result_Result_t U i32) := - Return (foo_foo U T traitInst) + Ok (foo_foo U T traitInst) . End Traits. |