diff --git a/tests/coq/misc/External_Funs.v b/tests/coq/misc/External_Funs.v index a3275de82..3594e22e2 100644 --- a/tests/coq/misc/External_Funs.v +++ b/tests/coq/misc/External_Funs.v @@ -12,13 +12,6 @@ Require Import External_FunsExternal. Include External_FunsExternal. Module External_Funs. -(** Trait implementation: [core::marker::{core::marker::Copy for u32}#40] - Source: '/rustc/library/core/src/marker.rs', lines 48:25-48:62 - Name pattern: core::marker::Copy *) -Definition core_marker_CopyU32 : core_marker_Copy_t u32 := {| - core_marker_Copy_tcore_marker_Copy_t_cloneCloneInst := core_clone_CloneU32; -|}. - (** [external::use_get]: Source: 'tests/src/external.rs', lines 9:0-11:1 *) Definition use_get diff --git a/tests/coq/misc/External_FunsExternal_Template.v b/tests/coq/misc/External_FunsExternal_Template.v index 4de5c5c34..c3002326a 100644 --- a/tests/coq/misc/External_FunsExternal_Template.v +++ b/tests/coq/misc/External_FunsExternal_Template.v @@ -15,7 +15,7 @@ Module External_FunsExternal_Template. Source: '/rustc/library/core/src/cell.rs', lines 540:4-540:32 Name pattern: core::cell::{core::cell::Cell<@T>}::get *) Axiom core_cell_Cell_get : - forall{T : Type} (markerCopyInst : core_marker_Copy_t T), + forall{T : Type} (markerCopyInst : core_marker_Copy T), core_cell_Cell_t T -> state -> result (state * T) . diff --git a/tests/coq/misc/External_Types.v b/tests/coq/misc/External_Types.v index 7601795ac..b42c2ecfe 100644 --- a/tests/coq/misc/External_Types.v +++ b/tests/coq/misc/External_Types.v @@ -10,14 +10,4 @@ Require Import External_TypesExternal. Include External_TypesExternal. Module External_Types. -(** Trait declaration: [core::marker::Copy] - Source: '/rustc/library/core/src/marker.rs', lines 416:0-416:21 - Name pattern: core::marker::Copy *) -Record core_marker_Copy_t (Self : Type) := mkcore_marker_Copy_t { - core_marker_Copy_tcore_marker_Copy_t_cloneCloneInst : core_clone_Clone Self; -}. - -Arguments mkcore_marker_Copy_t { _ }. -Arguments core_marker_Copy_tcore_marker_Copy_t_cloneCloneInst { _ } _. - End External_Types. diff --git a/tests/fstar/misc/External.Funs.fst b/tests/fstar/misc/External.Funs.fst index cba918b91..3208d825e 100644 --- a/tests/fstar/misc/External.Funs.fst +++ b/tests/fstar/misc/External.Funs.fst @@ -7,13 +7,6 @@ include External.FunsExternal #set-options "--z3rlimit 50 --fuel 1 --ifuel 1" -(** Trait implementation: [core::marker::{core::marker::Copy for u32}#40] - Source: '/rustc/library/core/src/marker.rs', lines 48:25-48:62 - Name pattern: core::marker::Copy *) -let core_marker_CopyU32 : core_marker_Copy_t u32 = { - cloneCloneInst = core_clone_CloneU32; -} - (** [external::use_get]: Source: 'tests/src/external.rs', lines 9:0-11:1 *) let use_get (rc : core_cell_Cell_t u32) (st : state) : result (state & u32) = diff --git a/tests/fstar/misc/External.FunsExternal.fsti b/tests/fstar/misc/External.FunsExternal.fsti index 4f1213966..9fca284e1 100644 --- a/tests/fstar/misc/External.FunsExternal.fsti +++ b/tests/fstar/misc/External.FunsExternal.fsti @@ -10,7 +10,7 @@ include External.Types Source: '/rustc/library/core/src/cell.rs', lines 540:4-540:32 Name pattern: core::cell::{core::cell::Cell<@T>}::get *) val core_cell_Cell_get - (#t : Type0) (markerCopyInst : core_marker_Copy_t t) : + (#t : Type0) (markerCopyInst : core_marker_Copy t) : core_cell_Cell_t t -> state -> result (state & t) (** [core::cell::{core::cell::Cell}#11::get_mut]: diff --git a/tests/fstar/misc/External.Types.fst b/tests/fstar/misc/External.Types.fst index cb4fa57bf..4fbcec476 100644 --- a/tests/fstar/misc/External.Types.fst +++ b/tests/fstar/misc/External.Types.fst @@ -6,10 +6,3 @@ include External.TypesExternal #set-options "--z3rlimit 50 --fuel 1 --ifuel 1" -(** Trait declaration: [core::marker::Copy] - Source: '/rustc/library/core/src/marker.rs', lines 416:0-416:21 - Name pattern: core::marker::Copy *) -noeq type core_marker_Copy_t (self : Type0) = { - cloneCloneInst : core_clone_Clone self; -} - diff --git a/tests/lean/External/Funs.lean b/tests/lean/External/Funs.lean index 5e2975eca..6df57acf7 100644 --- a/tests/lean/External/Funs.lean +++ b/tests/lean/External/Funs.lean @@ -10,14 +10,6 @@ set_option linter.unusedVariables false namespace external -/- Trait implementation: [core::marker::{core::marker::Copy for u32}#40] - Source: '/rustc/library/core/src/marker.rs', lines 48:25-48:62 - Name pattern: core::marker::Copy -/ -@[reducible] -def core.marker.CopyU32 : core.marker.Copy U32 := { - cloneCloneInst := core.clone.CloneU32 -} - /- [external::use_get]: Source: 'tests/src/external.rs', lines 9:0-11:1 -/ def use_get (rc : core.cell.Cell U32) (st : State) : Result (State × U32) := diff --git a/tests/lean/External/Types.lean b/tests/lean/External/Types.lean index 5e64121ed..789ce2b82 100644 --- a/tests/lean/External/Types.lean +++ b/tests/lean/External/Types.lean @@ -9,10 +9,4 @@ set_option linter.unusedVariables false namespace external -/- Trait declaration: [core::marker::Copy] - Source: '/rustc/library/core/src/marker.rs', lines 416:0-416:21 - Name pattern: core::marker::Copy -/ -structure core.marker.Copy (Self : Type) where - cloneCloneInst : core.clone.Clone Self - end external diff --git a/tests/lean/Traits.lean b/tests/lean/Traits.lean index 77374ce78..93b17b90c 100644 --- a/tests/lean/Traits.lean +++ b/tests/lean/Traits.lean @@ -518,13 +518,6 @@ structure Foo (T : Type) (U : Type) where x : T y : U -/- [core::result::Result] - Source: '/rustc/library/core/src/result.rs', lines 527:0-527:21 - Name pattern: core::result::Result -/ -inductive core.result.Result (T : Type) (E : Type) := -| Ok : T → core.result.Result T E -| Err : E → core.result.Result T E - /- [traits::{traits::Foo}#16::FOO] Source: 'tests/src/traits.rs', lines 334:4-334:43 -/ def Foo.FOO_body {T : Type} (U : Type) (TraitInst : Trait T) diff --git a/tests/src/mutually-recursive-traits.lean.out b/tests/src/mutually-recursive-traits.lean.out index 700af9ce2..a45c2bb0b 100644 --- a/tests/src/mutually-recursive-traits.lean.out +++ b/tests/src/mutually-recursive-traits.lean.out @@ -13,4 +13,4 @@ Called from Stdlib__List.iter in file "list.ml", line 110, characters 12-15 Called from Aeneas__Translate.extract_definitions in file "Translate.ml", line 879, characters 2-52 Called from Aeneas__Translate.extract_file in file "Translate.ml", line 1006, characters 2-36 Called from Aeneas__Translate.translate_crate in file "Translate.ml", line 1576, characters 5-42 -Called from Dune__exe__Main in file "Main.ml", line 336, characters 14-66 +Called from Dune__exe__Main in file "Main.ml", line 509, characters 14-66