summaryrefslogtreecommitdiff
path: root/tests
diff options
context:
space:
mode:
Diffstat (limited to 'tests')
-rw-r--r--tests/coq/traits/Traits.v107
-rw-r--r--tests/fstar/traits/Traits.fst106
-rw-r--r--tests/lean/Traits.lean104
3 files changed, 186 insertions, 131 deletions
diff --git a/tests/coq/traits/Traits.v b/tests/coq/traits/Traits.v
index 93ff9fe3..0952a1df 100644
--- a/tests/coq/traits/Traits.v
+++ b/tests/coq/traits/Traits.v
@@ -67,8 +67,8 @@ Definition test_bool_trait_option (T : Type) (x : option T) : result bool :=
(** [traits::test_bool_trait]: forward function
Source: 'src/traits.rs', lines 35:0-35:50 *)
Definition test_bool_trait
- (T : Type) (inst : BoolTrait_t T) (x : T) : result bool :=
- inst.(BoolTrait_t_get_bool) x
+ (T : Type) (boolTraitTInst : BoolTrait_t T) (x : T) : result bool :=
+ boolTraitTInst.(BoolTrait_t_get_bool) x
.
(** Trait declaration: [traits::ToU64]
@@ -94,30 +94,31 @@ Definition traits_ToU64U64Inst : ToU64_t u64 := {|
(** [traits::{(A, A)#3}::to_u64]: forward function
Source: 'src/traits.rs', lines 50:4-50:26 *)
Definition pair_to_u64
- (A : Type) (inst : ToU64_t A) (self : (A * A)) : result u64 :=
+ (A : Type) (toU64AInst : ToU64_t A) (self : (A * A)) : result u64 :=
let (t, t0) := self in
- i <- inst.(ToU64_t_to_u64) t;
- i0 <- inst.(ToU64_t_to_u64) t0;
+ i <- toU64AInst.(ToU64_t_to_u64) t;
+ i0 <- toU64AInst.(ToU64_t_to_u64) t0;
u64_add i i0
.
(** Trait implementation: [traits::{(A, A)#3}]
Source: 'src/traits.rs', lines 49:0-49:31 *)
-Definition traits_ToU64TupleAAInst (A : Type) (inst : ToU64_t A) : ToU64_t (A *
- A) := {|
- ToU64_t_to_u64 := pair_to_u64 A inst;
+Definition traits_ToU64TupleAAInst (A : Type) (toU64AInst : ToU64_t A) :
+ ToU64_t (A * A) := {|
+ ToU64_t_to_u64 := pair_to_u64 A toU64AInst;
|}.
(** [traits::f]: forward function
Source: 'src/traits.rs', lines 55:0-55:36 *)
-Definition f (T : Type) (inst : ToU64_t T) (x : (T * T)) : result u64 :=
- pair_to_u64 T inst x
+Definition f (T : Type) (toU64TInst : ToU64_t T) (x : (T * T)) : result u64 :=
+ pair_to_u64 T toU64TInst x
.
(** [traits::g]: forward function
Source: 'src/traits.rs', lines 59:0-61:18 *)
-Definition g (T : Type) (inst : ToU64_t (T * T)) (x : (T * T)) : result u64 :=
- inst.(ToU64_t_to_u64) x
+Definition g
+ (T : Type) (toU64TupleTTInst : ToU64_t (T * T)) (x : (T * T)) : result u64 :=
+ toU64TupleTTInst.(ToU64_t_to_u64) x
.
(** [traits::h0]: forward function
@@ -135,15 +136,15 @@ Arguments wrapper_x { _ }.
(** [traits::{traits::Wrapper<T>#4}::to_u64]: forward function
Source: 'src/traits.rs', lines 75:4-75:26 *)
Definition wrapper_to_u64
- (T : Type) (inst : ToU64_t T) (self : Wrapper_t T) : result u64 :=
- inst.(ToU64_t_to_u64) self.(wrapper_x)
+ (T : Type) (toU64TInst : ToU64_t T) (self : Wrapper_t T) : result u64 :=
+ toU64TInst.(ToU64_t_to_u64) self.(wrapper_x)
.
(** Trait implementation: [traits::{traits::Wrapper<T>#4}]
Source: 'src/traits.rs', lines 74:0-74:35 *)
-Definition traits_ToU64traitsWrapperTInst (T : Type) (inst : ToU64_t T) :
+Definition traits_ToU64traitsWrapperTInst (T : Type) (toU64TInst : ToU64_t T) :
ToU64_t (Wrapper_t T) := {|
- ToU64_t_to_u64 := wrapper_to_u64 T inst;
+ ToU64_t_to_u64 := wrapper_to_u64 T toU64TInst;
|}.
(** [traits::h1]: forward function
@@ -154,8 +155,9 @@ Definition h1 (x : Wrapper_t u64) : result u64 :=
(** [traits::h2]: forward function
Source: 'src/traits.rs', lines 84:0-84:41 *)
-Definition h2 (T : Type) (inst : ToU64_t T) (x : Wrapper_t T) : result u64 :=
- wrapper_to_u64 T inst x
+Definition h2
+ (T : Type) (toU64TInst : ToU64_t T) (x : Wrapper_t T) : result u64 :=
+ wrapper_to_u64 T toU64TInst x
.
(** Trait declaration: [traits::ToType]
@@ -181,8 +183,8 @@ Definition traits_ToTypeU64BoolInst : ToType_t u64 bool := {|
(** Trait declaration: [traits::OfType]
Source: 'src/traits.rs', lines 98:0-98:16 *)
Record OfType_t (Self : Type) := mkOfType_t {
- OfType_t_of_type : forall (T : Type) (inst : ToType_t T Self), T -> result
- Self;
+ OfType_t_of_type : forall (T : Type) (toTypeTSelfInst : ToType_t T Self), T
+ -> result Self;
}.
Arguments mkOfType_t { _ }.
@@ -191,10 +193,11 @@ Arguments OfType_t_of_type { _ }.
(** [traits::h3]: forward function
Source: 'src/traits.rs', lines 104:0-104:50 *)
Definition h3
- (T1 T2 : Type) (inst : OfType_t T1) (inst0 : ToType_t T2 T1) (y : T2) :
+ (T1 T2 : Type) (ofTypeT1Inst : OfType_t T1) (toTypeT2T1Inst : ToType_t T2 T1)
+ (y : T2) :
result T1
:=
- inst.(OfType_t_of_type) T2 inst0 y
+ ofTypeT1Inst.(OfType_t_of_type) T2 toTypeT2T1Inst y
.
(** Trait declaration: [traits::OfTypeBis]
@@ -211,10 +214,11 @@ Arguments OfTypeBis_t_of_type { _ _ }.
(** [traits::h4]: forward function
Source: 'src/traits.rs', lines 118:0-118:57 *)
Definition h4
- (T1 T2 : Type) (inst : OfTypeBis_t T1 T2) (inst0 : ToType_t T2 T1) (y : T2) :
+ (T1 T2 : Type) (ofTypeBisT1T2Inst : OfTypeBis_t T1 T2) (toTypeT2T1Inst :
+ ToType_t T2 T1) (y : T2) :
result T1
:=
- inst.(OfTypeBis_t_of_type) y
+ ofTypeBisT1T2Inst.(OfTypeBis_t_of_type) y
.
(** [traits::TestType]
@@ -258,8 +262,10 @@ Definition traits_TestType_test_TestTraittraitstraitsTestTypeTtestTestType1Inst
(** [traits::{traits::TestType<T>#6}::test]: forward function
Source: 'src/traits.rs', lines 126:4-126:36 *)
Definition testType_test
- (T : Type) (inst : ToU64_t T) (self : TestType_t T) (x : T) : result bool :=
- x0 <- inst.(ToU64_t_to_u64) x;
+ (T : Type) (toU64TInst : ToU64_t T) (self : TestType_t T) (x : T) :
+ result bool
+ :=
+ x0 <- toU64TInst.(ToU64_t_to_u64) x;
if x0 s> 0%u64
then testType_test_TestType1_test {| testType_test_TestType1_0 := 0%u64 |}
else Return false
@@ -272,15 +278,17 @@ Record BoolWrapper_t := mkBoolWrapper_t { boolWrapper_0 : bool; }.
(** [traits::{traits::BoolWrapper#7}::to_type]: forward function
Source: 'src/traits.rs', lines 156:4-156:25 *)
Definition boolWrapper_to_type
- (T : Type) (inst : ToType_t bool T) (self : BoolWrapper_t) : result T :=
- inst.(ToType_t_to_type) self.(boolWrapper_0)
+ (T : Type) (toTypeBoolTInst : ToType_t bool T) (self : BoolWrapper_t) :
+ result T
+ :=
+ toTypeBoolTInst.(ToType_t_to_type) self.(boolWrapper_0)
.
(** Trait implementation: [traits::{traits::BoolWrapper#7}]
Source: 'src/traits.rs', lines 152:0-152:33 *)
-Definition traits_ToTypetraitsBoolWrapperTInst (T : Type) (inst : ToType_t bool
- T) : ToType_t BoolWrapper_t T := {|
- ToType_t_to_type := boolWrapper_to_type T inst;
+Definition traits_ToTypetraitsBoolWrapperTInst (T : Type) (toTypeBoolTInst :
+ ToType_t bool T) : ToType_t BoolWrapper_t T := {|
+ ToType_t_to_type := boolWrapper_to_type T toTypeBoolTInst;
|}.
(** [traits::WithConstTy::LEN2]
@@ -333,15 +341,17 @@ Definition traits_WithConstTyBool32Inst : WithConstTy_t bool 32%usize := {|
(** [traits::use_with_const_ty1]: forward function
Source: 'src/traits.rs', lines 183:0-183:75 *)
Definition use_with_const_ty1
- (H : Type) (LEN : usize) (inst : WithConstTy_t H LEN) : result usize :=
- let i := inst.(WithConstTy_tWithConstTy_t_LEN1) in Return i
+ (H : Type) (LEN : usize) (withConstTyHLENInst : WithConstTy_t H LEN) :
+ result usize
+ :=
+ let i := withConstTyHLENInst.(WithConstTy_tWithConstTy_t_LEN1) in Return i
.
(** [traits::use_with_const_ty2]: forward function
Source: 'src/traits.rs', lines 187:0-187:73 *)
Definition use_with_const_ty2
- (H : Type) (LEN : usize) (inst : WithConstTy_t H LEN)
- (w : inst.(WithConstTy_tWithConstTy_t_W)) :
+ (H : Type) (LEN : usize) (withConstTyHLENInst : WithConstTy_t H LEN)
+ (w : withConstTyHLENInst.(WithConstTy_tWithConstTy_t_W)) :
result unit
:=
Return tt
@@ -350,11 +360,12 @@ Definition use_with_const_ty2
(** [traits::use_with_const_ty3]: forward function
Source: 'src/traits.rs', lines 189:0-189:80 *)
Definition use_with_const_ty3
- (H : Type) (LEN : usize) (inst : WithConstTy_t H LEN)
- (x : inst.(WithConstTy_tWithConstTy_t_W)) :
+ (H : Type) (LEN : usize) (withConstTyHLENInst : WithConstTy_t H LEN)
+ (x : withConstTyHLENInst.(WithConstTy_tWithConstTy_t_W)) :
result u64
:=
- inst.(WithConstTy_tWithConstTy_t_W_clause_0).(ToU64_t_to_u64) x
+ withConstTyHLENInst.(WithConstTy_tWithConstTy_t_W_clause_0).(ToU64_t_to_u64)
+ x
.
(** [traits::test_where1]: forward function
@@ -365,7 +376,9 @@ Definition test_where1 (T : Type) (_x : T) : result unit :=
(** [traits::test_where2]: forward function
Source: 'src/traits.rs', lines 194:0-194:57 *)
Definition test_where2
- (T : Type) (inst : WithConstTy_t T 32%usize) (_x : u32) : result unit :=
+ (T : Type) (withConstTyT32Inst : WithConstTy_t T 32%usize) (_x : u32) :
+ result unit
+ :=
Return tt
.
@@ -406,25 +419,29 @@ Arguments ChildTrait_tChildTrait_t_ParentTrait1SelfInst { _ }.
(** [traits::test_child_trait1]: forward function
Source: 'src/traits.rs', lines 209:0-209:56 *)
Definition test_child_trait1
- (T : Type) (inst : ChildTrait_t T) (x : T) : result alloc_string_String_t :=
- inst.(ChildTrait_tChildTrait_t_ParentTrait0SelfInst).(ParentTrait0_t_get_name)
+ (T : Type) (childTraitTInst : ChildTrait_t T) (x : T) :
+ result alloc_string_String_t
+ :=
+ childTraitTInst.(ChildTrait_tChildTrait_t_ParentTrait0SelfInst).(ParentTrait0_t_get_name)
x
.
(** [traits::test_child_trait2]: forward function
Source: 'src/traits.rs', lines 213:0-213:54 *)
Definition test_child_trait2
- (T : Type) (inst : ChildTrait_t T) (x : T) :
+ (T : Type) (childTraitTInst : ChildTrait_t T) (x : T) :
result
- inst.(ChildTrait_tChildTrait_t_ParentTrait0SelfInst).(ParentTrait0_tParentTrait0_t_W)
+ childTraitTInst.(ChildTrait_tChildTrait_t_ParentTrait0SelfInst).(ParentTrait0_tParentTrait0_t_W)
:=
- inst.(ChildTrait_tChildTrait_t_ParentTrait0SelfInst).(ParentTrait0_t_get_w) x
+ childTraitTInst.(ChildTrait_tChildTrait_t_ParentTrait0SelfInst).(ParentTrait0_t_get_w)
+ x
.
(** [traits::order1]: forward function
Source: 'src/traits.rs', lines 219:0-219:59 *)
Definition order1
- (T U : Type) (inst : ParentTrait0_t T) (inst0 : ParentTrait0_t U) :
+ (T U : Type) (parentTrait0TInst : ParentTrait0_t T) (parentTrait0UInst :
+ ParentTrait0_t U) :
result unit
:=
Return tt
diff --git a/tests/fstar/traits/Traits.fst b/tests/fstar/traits/Traits.fst
index 63ac307f..4cb9fbf1 100644
--- a/tests/fstar/traits/Traits.fst
+++ b/tests/fstar/traits/Traits.fst
@@ -54,8 +54,9 @@ let test_bool_trait_option (t : Type0) (x : option t) : result bool =
(** [traits::test_bool_trait]: forward function
Source: 'src/traits.rs', lines 35:0-35:50 *)
-let test_bool_trait (t : Type0) (inst : boolTrait_t t) (x : t) : result bool =
- inst.get_bool x
+let test_bool_trait
+ (t : Type0) (boolTraitTInst : boolTrait_t t) (x : t) : result bool =
+ boolTraitTInst.get_bool x
(** Trait declaration: [traits::ToU64]
Source: 'src/traits.rs', lines 39:0-39:15 *)
@@ -72,28 +73,30 @@ let traits_ToU64U64Inst : toU64_t u64 = { to_u64 = u64_to_u64; }
(** [traits::{(A, A)#3}::to_u64]: forward function
Source: 'src/traits.rs', lines 50:4-50:26 *)
-let pair_to_u64 (a : Type0) (inst : toU64_t a) (self : (a & a)) : result u64 =
+let pair_to_u64
+ (a : Type0) (toU64AInst : toU64_t a) (self : (a & a)) : result u64 =
let (x, x0) = self in
- let* i = inst.to_u64 x in
- let* i0 = inst.to_u64 x0 in
+ let* i = toU64AInst.to_u64 x in
+ let* i0 = toU64AInst.to_u64 x0 in
u64_add i i0
(** Trait implementation: [traits::{(A, A)#3}]
Source: 'src/traits.rs', lines 49:0-49:31 *)
-let traits_ToU64TupleAAInst (a : Type0) (inst : toU64_t a) : toU64_t (a & a)
- = {
- to_u64 = pair_to_u64 a inst;
+let traits_ToU64TupleAAInst (a : Type0) (toU64AInst : toU64_t a) : toU64_t (a &
+ a) = {
+ to_u64 = pair_to_u64 a toU64AInst;
}
(** [traits::f]: forward function
Source: 'src/traits.rs', lines 55:0-55:36 *)
-let f (t : Type0) (inst : toU64_t t) (x : (t & t)) : result u64 =
- pair_to_u64 t inst x
+let f (t : Type0) (toU64TInst : toU64_t t) (x : (t & t)) : result u64 =
+ pair_to_u64 t toU64TInst x
(** [traits::g]: forward function
Source: 'src/traits.rs', lines 59:0-61:18 *)
-let g (t : Type0) (inst : toU64_t (t & t)) (x : (t & t)) : result u64 =
- inst.to_u64 x
+let g
+ (t : Type0) (toU64TupleTTInst : toU64_t (t & t)) (x : (t & t)) : result u64 =
+ toU64TupleTTInst.to_u64 x
(** [traits::h0]: forward function
Source: 'src/traits.rs', lines 66:0-66:24 *)
@@ -107,14 +110,14 @@ type wrapper_t (t : Type0) = { x : t; }
(** [traits::{traits::Wrapper<T>#4}::to_u64]: forward function
Source: 'src/traits.rs', lines 75:4-75:26 *)
let wrapper_to_u64
- (t : Type0) (inst : toU64_t t) (self : wrapper_t t) : result u64 =
- inst.to_u64 self.x
+ (t : Type0) (toU64TInst : toU64_t t) (self : wrapper_t t) : result u64 =
+ toU64TInst.to_u64 self.x
(** Trait implementation: [traits::{traits::Wrapper<T>#4}]
Source: 'src/traits.rs', lines 74:0-74:35 *)
-let traits_ToU64traitsWrapperTInst (t : Type0) (inst : toU64_t t) : toU64_t
- (wrapper_t t) = {
- to_u64 = wrapper_to_u64 t inst;
+let traits_ToU64traitsWrapperTInst (t : Type0) (toU64TInst : toU64_t t) :
+ toU64_t (wrapper_t t) = {
+ to_u64 = wrapper_to_u64 t toU64TInst;
}
(** [traits::h1]: forward function
@@ -124,8 +127,8 @@ let h1 (x : wrapper_t u64) : result u64 =
(** [traits::h2]: forward function
Source: 'src/traits.rs', lines 84:0-84:41 *)
-let h2 (t : Type0) (inst : toU64_t t) (x : wrapper_t t) : result u64 =
- wrapper_to_u64 t inst x
+let h2 (t : Type0) (toU64TInst : toU64_t t) (x : wrapper_t t) : result u64 =
+ wrapper_to_u64 t toU64TInst x
(** Trait declaration: [traits::ToType]
Source: 'src/traits.rs', lines 88:0-88:19 *)
@@ -143,16 +146,18 @@ let traits_ToTypeU64BoolInst : toType_t u64 bool = { to_type = u64_to_type; }
(** Trait declaration: [traits::OfType]
Source: 'src/traits.rs', lines 98:0-98:16 *)
noeq type ofType_t (self : Type0) = {
- of_type : (t : Type0) -> (inst : toType_t t self) -> t -> result self;
+ of_type : (t : Type0) -> (toTypeTSelfInst : toType_t t self) -> t -> result
+ self;
}
(** [traits::h3]: forward function
Source: 'src/traits.rs', lines 104:0-104:50 *)
let h3
- (t1 t2 : Type0) (inst : ofType_t t1) (inst0 : toType_t t2 t1) (y : t2) :
+ (t1 t2 : Type0) (ofTypeT1Inst : ofType_t t1) (toTypeT2T1Inst : toType_t t2
+ t1) (y : t2) :
result t1
=
- inst.of_type t2 inst0 y
+ ofTypeT1Inst.of_type t2 toTypeT2T1Inst y
(** Trait declaration: [traits::OfTypeBis]
Source: 'src/traits.rs', lines 109:0-109:36 *)
@@ -164,11 +169,11 @@ noeq type ofTypeBis_t (self t : Type0) = {
(** [traits::h4]: forward function
Source: 'src/traits.rs', lines 118:0-118:57 *)
let h4
- (t1 t2 : Type0) (inst : ofTypeBis_t t1 t2) (inst0 : toType_t t2 t1)
- (y : t2) :
+ (t1 t2 : Type0) (ofTypeBisT1T2Inst : ofTypeBis_t t1 t2) (toTypeT2T1Inst :
+ toType_t t2 t1) (y : t2) :
result t1
=
- inst.of_type y
+ ofTypeBisT1T2Inst.of_type y
(** [traits::TestType]
Source: 'src/traits.rs', lines 122:0-122:22 *)
@@ -200,8 +205,10 @@ let traits_TestType_test_TestTraittraitstraitsTestTypeTtestTestType1Inst :
(** [traits::{traits::TestType<T>#6}::test]: forward function
Source: 'src/traits.rs', lines 126:4-126:36 *)
let testType_test
- (t : Type0) (inst : toU64_t t) (self : testType_t t) (x : t) : result bool =
- let* x0 = inst.to_u64 x in
+ (t : Type0) (toU64TInst : toU64_t t) (self : testType_t t) (x : t) :
+ result bool
+ =
+ let* x0 = toU64TInst.to_u64 x in
if x0 > 0 then testType_test_TestType1_test { _0 = 0 } else Return false
(** [traits::BoolWrapper]
@@ -211,14 +218,16 @@ type boolWrapper_t = { _0 : bool; }
(** [traits::{traits::BoolWrapper#7}::to_type]: forward function
Source: 'src/traits.rs', lines 156:4-156:25 *)
let boolWrapper_to_type
- (t : Type0) (inst : toType_t bool t) (self : boolWrapper_t) : result t =
- inst.to_type self._0
+ (t : Type0) (toTypeBoolTInst : toType_t bool t) (self : boolWrapper_t) :
+ result t
+ =
+ toTypeBoolTInst.to_type self._0
(** Trait implementation: [traits::{traits::BoolWrapper#7}]
Source: 'src/traits.rs', lines 152:0-152:33 *)
-let traits_ToTypetraitsBoolWrapperTInst (t : Type0) (inst : toType_t bool t) :
- toType_t boolWrapper_t t = {
- to_type = boolWrapper_to_type t inst;
+let traits_ToTypetraitsBoolWrapperTInst (t : Type0) (toTypeBoolTInst : toType_t
+ bool t) : toType_t boolWrapper_t t = {
+ to_type = boolWrapper_to_type t toTypeBoolTInst;
}
(** [traits::WithConstTy::LEN2]
@@ -262,13 +271,16 @@ let traits_WithConstTyBool32Inst : withConstTy_t bool 32 = {
(** [traits::use_with_const_ty1]: forward function
Source: 'src/traits.rs', lines 183:0-183:75 *)
let use_with_const_ty1
- (h : Type0) (len : usize) (inst : withConstTy_t h len) : result usize =
- let i = inst.cLEN1 in Return i
+ (h : Type0) (len : usize) (withConstTyHLENInst : withConstTy_t h len) :
+ result usize
+ =
+ let i = withConstTyHLENInst.cLEN1 in Return i
(** [traits::use_with_const_ty2]: forward function
Source: 'src/traits.rs', lines 187:0-187:73 *)
let use_with_const_ty2
- (h : Type0) (len : usize) (inst : withConstTy_t h len) (w : inst.tW) :
+ (h : Type0) (len : usize) (withConstTyHLENInst : withConstTy_t h len)
+ (w : withConstTyHLENInst.tW) :
result unit
=
Return ()
@@ -276,10 +288,11 @@ let use_with_const_ty2
(** [traits::use_with_const_ty3]: forward function
Source: 'src/traits.rs', lines 189:0-189:80 *)
let use_with_const_ty3
- (h : Type0) (len : usize) (inst : withConstTy_t h len) (x : inst.tW) :
+ (h : Type0) (len : usize) (withConstTyHLENInst : withConstTy_t h len)
+ (x : withConstTyHLENInst.tW) :
result u64
=
- inst.tW_clause_0.to_u64 x
+ withConstTyHLENInst.tW_clause_0.to_u64 x
(** [traits::test_where1]: forward function
Source: 'src/traits.rs', lines 193:0-193:40 *)
@@ -289,7 +302,9 @@ let test_where1 (t : Type0) (_x : t) : result unit =
(** [traits::test_where2]: forward function
Source: 'src/traits.rs', lines 194:0-194:57 *)
let test_where2
- (t : Type0) (inst : withConstTy_t t 32) (_x : u32) : result unit =
+ (t : Type0) (withConstTyT32Inst : withConstTy_t t 32) (_x : u32) :
+ result unit
+ =
Return ()
(** [alloc::string::String]
@@ -318,21 +333,24 @@ noeq type childTrait_t (self : Type0) = {
(** [traits::test_child_trait1]: forward function
Source: 'src/traits.rs', lines 209:0-209:56 *)
let test_child_trait1
- (t : Type0) (inst : childTrait_t t) (x : t) : result alloc_string_String_t =
- inst.parentTrait0SelfInst.get_name x
+ (t : Type0) (childTraitTInst : childTrait_t t) (x : t) :
+ result alloc_string_String_t
+ =
+ childTraitTInst.parentTrait0SelfInst.get_name x
(** [traits::test_child_trait2]: forward function
Source: 'src/traits.rs', lines 213:0-213:54 *)
let test_child_trait2
- (t : Type0) (inst : childTrait_t t) (x : t) :
- result inst.parentTrait0SelfInst.tW
+ (t : Type0) (childTraitTInst : childTrait_t t) (x : t) :
+ result childTraitTInst.parentTrait0SelfInst.tW
=
- inst.parentTrait0SelfInst.get_w x
+ childTraitTInst.parentTrait0SelfInst.get_w x
(** [traits::order1]: forward function
Source: 'src/traits.rs', lines 219:0-219:59 *)
let order1
- (t u : Type0) (inst : parentTrait0_t t) (inst0 : parentTrait0_t u) :
+ (t u : Type0) (parentTrait0TInst : parentTrait0_t t) (parentTrait0UInst :
+ parentTrait0_t u) :
result unit
=
Return ()
diff --git a/tests/lean/Traits.lean b/tests/lean/Traits.lean
index 0aa68c5e..9ac4736c 100644
--- a/tests/lean/Traits.lean
+++ b/tests/lean/Traits.lean
@@ -61,8 +61,9 @@ def test_bool_trait_option (T : Type) (x : Option T) : Result Bool :=
/- [traits::test_bool_trait]: forward function
Source: 'src/traits.rs', lines 35:0-35:50 -/
-def test_bool_trait (T : Type) (inst : BoolTrait T) (x : T) : Result Bool :=
- inst.get_bool x
+def test_bool_trait
+ (T : Type) (BoolTraitTInst : BoolTrait T) (x : T) : Result Bool :=
+ BoolTraitTInst.get_bool x
/- Trait declaration: [traits::ToU64]
Source: 'src/traits.rs', lines 39:0-39:15 -/
@@ -82,28 +83,31 @@ def traits.ToU64U64Inst : ToU64 U64 := {
/- [traits::{(A, A)#3}::to_u64]: forward function
Source: 'src/traits.rs', lines 50:4-50:26 -/
-def Pair.to_u64 (A : Type) (inst : ToU64 A) (self : (A × A)) : Result U64 :=
+def Pair.to_u64
+ (A : Type) (ToU64AInst : ToU64 A) (self : (A × A)) : Result U64 :=
do
let (t, t0) := self
- let i ← inst.to_u64 t
- let i0 ← inst.to_u64 t0
+ let i ← ToU64AInst.to_u64 t
+ let i0 ← ToU64AInst.to_u64 t0
i + i0
/- Trait implementation: [traits::{(A, A)#3}]
Source: 'src/traits.rs', lines 49:0-49:31 -/
-def traits.ToU64TupleAAInst (A : Type) (inst : ToU64 A) : ToU64 (A × A) := {
- to_u64 := Pair.to_u64 A inst
+def traits.ToU64TupleAAInst (A : Type) (ToU64AInst : ToU64 A) : ToU64 (A × A)
+ := {
+ to_u64 := Pair.to_u64 A ToU64AInst
}
/- [traits::f]: forward function
Source: 'src/traits.rs', lines 55:0-55:36 -/
-def f (T : Type) (inst : ToU64 T) (x : (T × T)) : Result U64 :=
- Pair.to_u64 T inst x
+def f (T : Type) (ToU64TInst : ToU64 T) (x : (T × T)) : Result U64 :=
+ Pair.to_u64 T ToU64TInst x
/- [traits::g]: forward function
Source: 'src/traits.rs', lines 59:0-61:18 -/
-def g (T : Type) (inst : ToU64 (T × T)) (x : (T × T)) : Result U64 :=
- inst.to_u64 x
+def g
+ (T : Type) (ToU64TupleTTInst : ToU64 (T × T)) (x : (T × T)) : Result U64 :=
+ ToU64TupleTTInst.to_u64 x
/- [traits::h0]: forward function
Source: 'src/traits.rs', lines 66:0-66:24 -/
@@ -118,14 +122,14 @@ structure Wrapper (T : Type) where
/- [traits::{traits::Wrapper<T>#4}::to_u64]: forward function
Source: 'src/traits.rs', lines 75:4-75:26 -/
def Wrapper.to_u64
- (T : Type) (inst : ToU64 T) (self : Wrapper T) : Result U64 :=
- inst.to_u64 self.x
+ (T : Type) (ToU64TInst : ToU64 T) (self : Wrapper T) : Result U64 :=
+ ToU64TInst.to_u64 self.x
/- Trait implementation: [traits::{traits::Wrapper<T>#4}]
Source: 'src/traits.rs', lines 74:0-74:35 -/
-def traits.ToU64traitsWrapperTInst (T : Type) (inst : ToU64 T) : ToU64 (Wrapper
- T) := {
- to_u64 := Wrapper.to_u64 T inst
+def traits.ToU64traitsWrapperTInst (T : Type) (ToU64TInst : ToU64 T) : ToU64
+ (Wrapper T) := {
+ to_u64 := Wrapper.to_u64 T ToU64TInst
}
/- [traits::h1]: forward function
@@ -135,8 +139,8 @@ def h1 (x : Wrapper U64) : Result U64 :=
/- [traits::h2]: forward function
Source: 'src/traits.rs', lines 84:0-84:41 -/
-def h2 (T : Type) (inst : ToU64 T) (x : Wrapper T) : Result U64 :=
- Wrapper.to_u64 T inst x
+def h2 (T : Type) (ToU64TInst : ToU64 T) (x : Wrapper T) : Result U64 :=
+ Wrapper.to_u64 T ToU64TInst x
/- Trait declaration: [traits::ToType]
Source: 'src/traits.rs', lines 88:0-88:19 -/
@@ -157,15 +161,17 @@ def traits.ToTypeU64BoolInst : ToType U64 Bool := {
/- Trait declaration: [traits::OfType]
Source: 'src/traits.rs', lines 98:0-98:16 -/
structure OfType (Self : Type) where
- of_type : forall (T : Type) (inst : ToType T Self), T → Result Self
+ of_type : forall (T : Type) (ToTypeTSelfInst : ToType T Self), T → Result
+ Self
/- [traits::h3]: forward function
Source: 'src/traits.rs', lines 104:0-104:50 -/
def h3
- (T1 T2 : Type) (inst : OfType T1) (inst0 : ToType T2 T1) (y : T2) :
+ (T1 T2 : Type) (OfTypeT1Inst : OfType T1) (ToTypeT2T1Inst : ToType T2 T1)
+ (y : T2) :
Result T1
:=
- inst.of_type T2 inst0 y
+ OfTypeT1Inst.of_type T2 ToTypeT2T1Inst y
/- Trait declaration: [traits::OfTypeBis]
Source: 'src/traits.rs', lines 109:0-109:36 -/
@@ -176,10 +182,11 @@ structure OfTypeBis (Self T : Type) where
/- [traits::h4]: forward function
Source: 'src/traits.rs', lines 118:0-118:57 -/
def h4
- (T1 T2 : Type) (inst : OfTypeBis T1 T2) (inst0 : ToType T2 T1) (y : T2) :
+ (T1 T2 : Type) (OfTypeBisT1T2Inst : OfTypeBis T1 T2) (ToTypeT2T1Inst : ToType
+ T2 T1) (y : T2) :
Result T1
:=
- inst.of_type y
+ OfTypeBisT1T2Inst.of_type y
/- [traits::TestType]
Source: 'src/traits.rs', lines 122:0-122:22 -/
@@ -212,9 +219,11 @@ def traits.TestType.test.TestTraittraitstraitsTestTypeTtestTestType1Inst :
/- [traits::{traits::TestType<T>#6}::test]: forward function
Source: 'src/traits.rs', lines 126:4-126:36 -/
def TestType.test
- (T : Type) (inst : ToU64 T) (self : TestType T) (x : T) : Result Bool :=
+ (T : Type) (ToU64TInst : ToU64 T) (self : TestType T) (x : T) :
+ Result Bool
+ :=
do
- let x0 ← inst.to_u64 x
+ let x0 ← ToU64TInst.to_u64 x
if x0 > 0#u64
then TestType.test.TestType1.test { _0 := 0#u64 }
else Result.ret false
@@ -227,14 +236,16 @@ structure BoolWrapper where
/- [traits::{traits::BoolWrapper#7}::to_type]: forward function
Source: 'src/traits.rs', lines 156:4-156:25 -/
def BoolWrapper.to_type
- (T : Type) (inst : ToType Bool T) (self : BoolWrapper) : Result T :=
- inst.to_type self._0
+ (T : Type) (ToTypeBoolTInst : ToType Bool T) (self : BoolWrapper) :
+ Result T
+ :=
+ ToTypeBoolTInst.to_type self._0
/- Trait implementation: [traits::{traits::BoolWrapper#7}]
Source: 'src/traits.rs', lines 152:0-152:33 -/
-def traits.ToTypetraitsBoolWrapperTInst (T : Type) (inst : ToType Bool T) :
- ToType BoolWrapper T := {
- to_type := BoolWrapper.to_type T inst
+def traits.ToTypetraitsBoolWrapperTInst (T : Type) (ToTypeBoolTInst : ToType
+ Bool T) : ToType BoolWrapper T := {
+ to_type := BoolWrapper.to_type T ToTypeBoolTInst
}
/- [traits::WithConstTy::LEN2]
@@ -278,14 +289,17 @@ def traits.WithConstTyBool32Inst : WithConstTy Bool 32#usize := {
/- [traits::use_with_const_ty1]: forward function
Source: 'src/traits.rs', lines 183:0-183:75 -/
def use_with_const_ty1
- (H : Type) (LEN : Usize) (inst : WithConstTy H LEN) : Result Usize :=
- let i := inst.LEN1
+ (H : Type) (LEN : Usize) (WithConstTyHLENInst : WithConstTy H LEN) :
+ Result Usize
+ :=
+ let i := WithConstTyHLENInst.LEN1
Result.ret i
/- [traits::use_with_const_ty2]: forward function
Source: 'src/traits.rs', lines 187:0-187:73 -/
def use_with_const_ty2
- (H : Type) (LEN : Usize) (inst : WithConstTy H LEN) (w : inst.W) :
+ (H : Type) (LEN : Usize) (WithConstTyHLENInst : WithConstTy H LEN)
+ (w : WithConstTyHLENInst.W) :
Result Unit
:=
Result.ret ()
@@ -293,10 +307,11 @@ def use_with_const_ty2
/- [traits::use_with_const_ty3]: forward function
Source: 'src/traits.rs', lines 189:0-189:80 -/
def use_with_const_ty3
- (H : Type) (LEN : Usize) (inst : WithConstTy H LEN) (x : inst.W) :
+ (H : Type) (LEN : Usize) (WithConstTyHLENInst : WithConstTy H LEN)
+ (x : WithConstTyHLENInst.W) :
Result U64
:=
- inst.W_clause_0.to_u64 x
+ WithConstTyHLENInst.W_clause_0.to_u64 x
/- [traits::test_where1]: forward function
Source: 'src/traits.rs', lines 193:0-193:40 -/
@@ -306,7 +321,9 @@ def test_where1 (T : Type) (_x : T) : Result Unit :=
/- [traits::test_where2]: forward function
Source: 'src/traits.rs', lines 194:0-194:57 -/
def test_where2
- (T : Type) (inst : WithConstTy T 32#usize) (_x : U32) : Result Unit :=
+ (T : Type) (WithConstTyT32Inst : WithConstTy T 32#usize) (_x : U32) :
+ Result Unit
+ :=
Result.ret ()
/- [alloc::string::String]
@@ -333,21 +350,24 @@ structure ChildTrait (Self : Type) where
/- [traits::test_child_trait1]: forward function
Source: 'src/traits.rs', lines 209:0-209:56 -/
def test_child_trait1
- (T : Type) (inst : ChildTrait T) (x : T) : Result alloc.string.String :=
- inst.ParentTrait0SelfInst.get_name x
+ (T : Type) (ChildTraitTInst : ChildTrait T) (x : T) :
+ Result alloc.string.String
+ :=
+ ChildTraitTInst.ParentTrait0SelfInst.get_name x
/- [traits::test_child_trait2]: forward function
Source: 'src/traits.rs', lines 213:0-213:54 -/
def test_child_trait2
- (T : Type) (inst : ChildTrait T) (x : T) :
- Result inst.ParentTrait0SelfInst.W
+ (T : Type) (ChildTraitTInst : ChildTrait T) (x : T) :
+ Result ChildTraitTInst.ParentTrait0SelfInst.W
:=
- inst.ParentTrait0SelfInst.get_w x
+ ChildTraitTInst.ParentTrait0SelfInst.get_w x
/- [traits::order1]: forward function
Source: 'src/traits.rs', lines 219:0-219:59 -/
def order1
- (T U : Type) (inst : ParentTrait0 T) (inst0 : ParentTrait0 U) :
+ (T U : Type) (ParentTrait0TInst : ParentTrait0 T) (ParentTrait0UInst :
+ ParentTrait0 U) :
Result Unit
:=
Result.ret ()
generated by cgit v1.2.3 (git 2.25.1) at 2024-10-18 21:18:06 +0000