Skip to content

Update charon #1091

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
Nadrieril merged 1 commit into from
May 31, 2026
Merged

Update charon #1091

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
8 changes: 4 additions & 4 deletions backends/lean/Aeneas/Std/Core/Cmp.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -13,12 +13,12 @@ structure core.cmp.PartialEq (Self : Type) (Rhs : Type) where
@[rust_trait "core::cmp::Eq" (parentClauses := ["partialEqInst"])]
structure core.cmp.Eq (Self : Type) where
partialEqInst : core.cmp.PartialEq Self Self
assert_receiver_is_total_eq (_ : Self) : Result Unit := .ok ()
assert_fields_are_eq (_ : Self) : Result Unit := .ok ()

@[simp, rust_fun "core::cmp::Eq::assert_receiver_is_total_eq"]
def core.cmp.Eq.assert_receiver_is_total_eq.default
@[simp, rust_fun "core::cmp::Eq::assert_fields_are_eq"]
def core.cmp.Eq.assert_fields_are_eq.default
{Self : Type} (EqInst : core.cmp.Eq Self) (x : Self) : Result Unit :=
EqInst.assert_receiver_is_total_eq x
EqInst.assert_fields_are_eq x

/- Default method -/
@[rust_fun "core::cmp::PartialEq::ne"]
Expand Down
2 changes: 1 addition & 1 deletion charon-pin
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,2 +1,2 @@
# This is the commit from https://github.com/AeneasVerif/charon that should be used with this version of aeneas.
d986428c0225810607e95f858a5b07afcfd15f92
42836b36b666a980cbc9d438a8aed340ad3b848b
14 changes: 7 additions & 7 deletions flake.lock
View file
Open in desktop

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

7 changes: 3 additions & 4 deletions src/extract/ExtractBuiltinLean.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -383,8 +383,8 @@ let lean_builtin_funs =
mk_fun "core::clone::impls::{core::clone::Clone<&'0 @T>}::clone"
"core.clone.impls.CloneShared.clone";
(* file: "Aeneas/Std/Core/Cmp.lean", line: 18 *)
mk_fun "core::cmp::Eq::assert_receiver_is_total_eq"
"core.cmp.Eq.assert_receiver_is_total_eq.default";
mk_fun "core::cmp::Eq::assert_fields_are_eq"
"core.cmp.Eq.assert_fields_are_eq.default";
(* file: "Aeneas/Std/Core/Cmp.lean", line: 98 *)
mk_fun "core::cmp::Ord::clamp" "core.cmp.Ord.clamp.default";
(* file: "Aeneas/Std/Core/Cmp.lean", line: 86 *)
Expand Down Expand Up @@ -948,8 +948,7 @@ let lean_builtin_trait_decls =
(* file: "Aeneas/Std/Core/Cmp.lean", line: 13 *)
mk_trait_decl "core::cmp::Eq" "core.cmp.Eq"
~parent_clauses:[ "partialEqInst" ]
~methods:
[ ("assert_receiver_is_total_eq", "assert_receiver_is_total_eq") ];
~methods:[ ("assert_fields_are_eq", "assert_fields_are_eq") ];
(* file: "Aeneas/Std/Core/Cmp.lean", line: 76 *)
mk_trait_decl "core::cmp::Ord" "core.cmp.Ord"
~parent_clauses:[ "eqInst"; "partialOrdInst" ]
Expand Down
4 changes: 2 additions & 2 deletions tests/coq/demo/Demo.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -9,13 +9,13 @@ Local Open Scope Primitives_scope.
Module Demo.

(** [core::num::{u32}::wrapping_add]:
Source: '/rustc/library/core/src/num/uint_macros.rs', lines 2456:8-2456:58
Source: '/rustc/library/core/src/num/uint_macros.rs', lines 2505:8-2505:58
Name pattern: [core::num::{u32}::wrapping_add]
Visibility: public *)
Axiom core_num_U32_wrapping_add : u32 -> u32 -> result u32.

(** [core::num::{u32}::wrapping_sub]:
Source: '/rustc/library/core/src/num/uint_macros.rs', lines 2493:8-2493:58
Source: '/rustc/library/core/src/num/uint_macros.rs', lines 2542:8-2542:58
Name pattern: [core::num::{u32}::wrapping_sub]
Visibility: public *)
Axiom core_num_U32_wrapping_sub : u32 -> u32 -> result u32.
Expand Down
2 changes: 1 addition & 1 deletion tests/coq/misc/DefaultedMethod.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -9,7 +9,7 @@ Local Open Scope Primitives_scope.
Module DefaultedMethod.

(** [core::cmp::impls::{impl core::cmp::Ord for i32}::min]:
Source: '/rustc/library/core/src/cmp.rs', lines 2000:12-2000:33
Source: '/rustc/library/core/src/cmp.rs', lines 2007:12-2007:33
Name pattern: [core::cmp::impls::{core::cmp::Ord<i32>}::min]
Visibility: public *)
Axiom I32_Insts_CoreCmpOrd_min : i32 -> i32 -> result i32.
Expand Down
4 changes: 2 additions & 2 deletions tests/fstar/demo/Demo.fst
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,13 +6,13 @@ open Primitives
#set-options "--z3rlimit 50 --fuel 1 --ifuel 1"

(** [core::num::{u32}::wrapping_add]:
Source: '/rustc/library/core/src/num/uint_macros.rs', lines 2456:8-2456:58
Source: '/rustc/library/core/src/num/uint_macros.rs', lines 2505:8-2505:58
Name pattern: [core::num::{u32}::wrapping_add]
Visibility: public *)
assume val core_num_U32_wrapping_add : u32 -> u32 -> result u32

(** [core::num::{u32}::wrapping_sub]:
Source: '/rustc/library/core/src/num/uint_macros.rs', lines 2493:8-2493:58
Source: '/rustc/library/core/src/num/uint_macros.rs', lines 2542:8-2542:58
Name pattern: [core::num::{u32}::wrapping_sub]
Visibility: public *)
assume val core_num_U32_wrapping_sub : u32 -> u32 -> result u32
Expand Down
2 changes: 1 addition & 1 deletion tests/fstar/misc/DefaultedMethod.fst
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,7 @@ open Primitives
#set-options "--z3rlimit 50 --fuel 1 --ifuel 1"

(** [core::cmp::impls::{impl core::cmp::Ord for i32}::min]:
Source: '/rustc/library/core/src/cmp.rs', lines 2000:12-2000:33
Source: '/rustc/library/core/src/cmp.rs', lines 2007:12-2007:33
Name pattern: [core::cmp::impls::{core::cmp::Ord<i32>}::min]
Visibility: public *)
assume val i32_Insts_CoreCmpOrd_min : i32 -> i32 -> result i32
Expand Down
2 changes: 1 addition & 1 deletion tests/lean/BuiltinAuto.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -18,7 +18,7 @@ noncomputable section
namespace builtin_auto

/-- [core::ptr::null]:
Source: '/rustc/library/core/src/ptr/mod.rs', lines 837:0-837:55
Source: '/rustc/library/core/src/ptr/mod.rs', lines 842:0-842:55
Name pattern: [core::ptr::null]
Visibility: public -/
@[rust_fun "core::ptr::null"]
Expand Down
66 changes: 32 additions & 34 deletions tests/lean/Derive.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -18,14 +18,14 @@ noncomputable section
namespace derive

/-- [core::cmp::impls::{impl core::cmp::PartialEq<bool> for bool}::ne]:
Source: '/rustc/library/core/src/cmp.rs', lines 1872:16-1872:50
Source: '/rustc/library/core/src/cmp.rs', lines 1879:16-1879:50
Name pattern: [core::cmp::impls::{core::cmp::PartialEq<bool, bool>}::ne]
Visibility: public -/
@[rust_fun "core::cmp::impls::{core::cmp::PartialEq<bool, bool>}::ne"]
axiom Bool.Insts.CoreCmpPartialEqBool.ne : Bool → Bool → Result Bool

/-- [alloc::boxed::{impl core::cmp::PartialEq<alloc::boxed::Box<T>> for alloc::boxed::Box<T>}::ne]:
Source: '/rustc/library/alloc/src/boxed.rs', lines 2100:4-2100:38
Source: '/rustc/library/alloc/src/boxed.rs', lines 2109:4-2109:38
Name pattern: [alloc::boxed::{core::cmp::PartialEq<Box<@T>, Box<@T>>}::ne]
Visibility: public -/
@[rust_fun "alloc::boxed::{core::cmp::PartialEq<Box<@T>, Box<@T>>}::ne"]
Expand Down Expand Up @@ -93,10 +93,10 @@ def CopyEnumOneVariant.Insts.CoreCmpPartialEqCopyEnumOneVariant :
ne := CopyEnumOneVariant.Insts.CoreCmpPartialEqCopyEnumOneVariant.ne
}

/-- [derive::{impl core::cmp::Eq for derive::CopyEnumOneVariant}::assert_receiver_is_total_eq]:
/-- [derive::{impl core::cmp::Eq for derive::CopyEnumOneVariant}::assert_fields_are_eq]:
Source: 'tests/src/derive.rs', lines 3:33-3:35
Visibility: public -/
def CopyEnumOneVariant.Insts.CoreCmpEq.assert_receiver_is_total_eq
def CopyEnumOneVariant.Insts.CoreCmpEq.assert_fields_are_eq
(self : CopyEnumOneVariant) : Result Unit := do
ok ()

Expand All @@ -105,8 +105,8 @@ def CopyEnumOneVariant.Insts.CoreCmpEq.assert_receiver_is_total_eq
@[reducible]
def CopyEnumOneVariant.Insts.CoreCmpEq : core.cmp.Eq CopyEnumOneVariant := {
partialEqInst := CopyEnumOneVariant.Insts.CoreCmpPartialEqCopyEnumOneVariant
assert_receiver_is_total_eq :=
CopyEnumOneVariant.Insts.CoreCmpEq.assert_receiver_is_total_eq
assert_fields_are_eq :=
CopyEnumOneVariant.Insts.CoreCmpEq.assert_fields_are_eq
}

/-- [derive::{impl core::fmt::Debug for derive::CopyEnumOneVariant}::fmt]:
Expand Down Expand Up @@ -189,10 +189,10 @@ def ScalarEnum.Insts.CoreCmpPartialEqScalarEnum : core.cmp.PartialEq ScalarEnum
ne := ScalarEnum.Insts.CoreCmpPartialEqScalarEnum.ne
}

/-- [derive::{impl core::cmp::Eq for derive::ScalarEnum}::assert_receiver_is_total_eq]:
/-- [derive::{impl core::cmp::Eq for derive::ScalarEnum}::assert_fields_are_eq]:
Source: 'tests/src/derive.rs', lines 8:33-8:35
Visibility: public -/
def ScalarEnum.Insts.CoreCmpEq.assert_receiver_is_total_eq
def ScalarEnum.Insts.CoreCmpEq.assert_fields_are_eq
(self : ScalarEnum) : Result Unit := do
ok ()

Expand All @@ -201,8 +201,7 @@ def ScalarEnum.Insts.CoreCmpEq.assert_receiver_is_total_eq
@[reducible]
def ScalarEnum.Insts.CoreCmpEq : core.cmp.Eq ScalarEnum := {
partialEqInst := ScalarEnum.Insts.CoreCmpPartialEqScalarEnum
assert_receiver_is_total_eq :=
ScalarEnum.Insts.CoreCmpEq.assert_receiver_is_total_eq
assert_fields_are_eq := ScalarEnum.Insts.CoreCmpEq.assert_fields_are_eq
}

/-- [derive::{impl core::fmt::Debug for derive::ScalarEnum}::fmt]:
Expand Down Expand Up @@ -330,10 +329,10 @@ def CopyEnum.Insts.CoreCmpPartialEqCopyEnum {T : Type} (corecmpPartialEqInst :
ne := CopyEnum.Insts.CoreCmpPartialEqCopyEnum.ne corecmpPartialEqInst
}

/-- [derive::{impl core::cmp::Eq for derive::CopyEnum<T>}::assert_receiver_is_total_eq]:
/-- [derive::{impl core::cmp::Eq for derive::CopyEnum<T>}::assert_fields_are_eq]:
Source: 'tests/src/derive.rs', lines 16:33-16:35
Visibility: public -/
def CopyEnum.Insts.CoreCmpEq.assert_receiver_is_total_eq
def CopyEnum.Insts.CoreCmpEq.assert_fields_are_eq
{T : Type} (corecmpEqInst : core.cmp.Eq T) (self : CopyEnum T) :
Result Unit
:= do
Expand All @@ -346,8 +345,8 @@ def CopyEnum.Insts.CoreCmpEq {T : Type} (corecmpEqInst : core.cmp.Eq T) :
core.cmp.Eq (CopyEnum T) := {
partialEqInst := CopyEnum.Insts.CoreCmpPartialEqCopyEnum
corecmpEqInst.partialEqInst
assert_receiver_is_total_eq :=
CopyEnum.Insts.CoreCmpEq.assert_receiver_is_total_eq corecmpEqInst
assert_fields_are_eq := CopyEnum.Insts.CoreCmpEq.assert_fields_are_eq
corecmpEqInst
}

/-- [derive::{impl core::fmt::Debug for derive::CopyEnum<T>}::fmt]:
Expand Down Expand Up @@ -492,10 +491,10 @@ def Enum.Insts.CoreCmpPartialEqEnum {T : Type} (corecmpPartialEqInst :
ne := Enum.Insts.CoreCmpPartialEqEnum.ne corecmpPartialEqInst
}

/-- [derive::{impl core::cmp::Eq for derive::Enum<T>}::assert_receiver_is_total_eq]:
/-- [derive::{impl core::cmp::Eq for derive::Enum<T>}::assert_fields_are_eq]:
Source: 'tests/src/derive.rs', lines 24:27-24:29
Visibility: public -/
def Enum.Insts.CoreCmpEq.assert_receiver_is_total_eq
def Enum.Insts.CoreCmpEq.assert_fields_are_eq
{T : Type} (corecmpEqInst : core.cmp.Eq T) (self : Enum T) :
Result Unit
:= do
Expand All @@ -507,8 +506,8 @@ def Enum.Insts.CoreCmpEq.assert_receiver_is_total_eq
def Enum.Insts.CoreCmpEq {T : Type} (corecmpEqInst : core.cmp.Eq T) :
core.cmp.Eq (Enum T) := {
partialEqInst := Enum.Insts.CoreCmpPartialEqEnum corecmpEqInst.partialEqInst
assert_receiver_is_total_eq :=
Enum.Insts.CoreCmpEq.assert_receiver_is_total_eq corecmpEqInst
assert_fields_are_eq := Enum.Insts.CoreCmpEq.assert_fields_are_eq
corecmpEqInst
}

/-- [derive::{impl core::fmt::Debug for derive::Enum<T>}::fmt]:
Expand Down Expand Up @@ -627,10 +626,10 @@ def List.Insts.CoreCmpPartialEqList {T : Type} (corecmpPartialEqInst :
ne := List.Insts.CoreCmpPartialEqList.ne corecmpPartialEqInst
}

/-- [derive::{impl core::cmp::Eq for derive::List<T>}::assert_receiver_is_total_eq]:
/-- [derive::{impl core::cmp::Eq for derive::List<T>}::assert_fields_are_eq]:
Source: 'tests/src/derive.rs', lines 34:27-34:29
Visibility: public -/
def List.Insts.CoreCmpEq.assert_receiver_is_total_eq
def List.Insts.CoreCmpEq.assert_fields_are_eq
{T : Type} (corecmpEqInst : core.cmp.Eq T) (self : List T) :
Result Unit
:= do
Expand All @@ -642,8 +641,8 @@ def List.Insts.CoreCmpEq.assert_receiver_is_total_eq
def List.Insts.CoreCmpEq {T : Type} (corecmpEqInst : core.cmp.Eq T) :
core.cmp.Eq (List T) := {
partialEqInst := List.Insts.CoreCmpPartialEqList corecmpEqInst.partialEqInst
assert_receiver_is_total_eq :=
List.Insts.CoreCmpEq.assert_receiver_is_total_eq corecmpEqInst
assert_fields_are_eq := List.Insts.CoreCmpEq.assert_fields_are_eq
corecmpEqInst
}

/-- [derive::CopyStruct]
Expand Down Expand Up @@ -726,10 +725,10 @@ def CopyStruct.Insts.CoreCmpPartialEqCopyStruct {T : Type}
ne := CopyStruct.Insts.CoreCmpPartialEqCopyStruct.ne corecmpPartialEqInst
}

/-- [derive::{impl core::cmp::Eq for derive::CopyStruct<T>}::assert_receiver_is_total_eq]:
/-- [derive::{impl core::cmp::Eq for derive::CopyStruct<T>}::assert_fields_are_eq]:
Source: 'tests/src/derive.rs', lines 41:33-41:35
Visibility: public -/
def CopyStruct.Insts.CoreCmpEq.assert_receiver_is_total_eq
def CopyStruct.Insts.CoreCmpEq.assert_fields_are_eq
{T : Type} (corecmpEqInst : core.cmp.Eq T) (self : CopyStruct T) :
Result Unit
:= do
Expand All @@ -742,8 +741,8 @@ def CopyStruct.Insts.CoreCmpEq {T : Type} (corecmpEqInst : core.cmp.Eq T) :
core.cmp.Eq (CopyStruct T) := {
partialEqInst := CopyStruct.Insts.CoreCmpPartialEqCopyStruct
corecmpEqInst.partialEqInst
assert_receiver_is_total_eq :=
CopyStruct.Insts.CoreCmpEq.assert_receiver_is_total_eq corecmpEqInst
assert_fields_are_eq := CopyStruct.Insts.CoreCmpEq.assert_fields_are_eq
corecmpEqInst
}

/-- [derive::{impl core::fmt::Debug for derive::CopyStruct<T>}::fmt]:
Expand Down Expand Up @@ -825,10 +824,10 @@ def Struct.Insts.CoreCmpPartialEqStruct {T : Type} (corecmpPartialEqInst :
ne := Struct.Insts.CoreCmpPartialEqStruct.ne corecmpPartialEqInst
}

/-- [derive::{impl core::cmp::Eq for derive::Struct<T>}::assert_receiver_is_total_eq]:
/-- [derive::{impl core::cmp::Eq for derive::Struct<T>}::assert_fields_are_eq]:
Source: 'tests/src/derive.rs', lines 49:27-49:29
Visibility: public -/
def Struct.Insts.CoreCmpEq.assert_receiver_is_total_eq
def Struct.Insts.CoreCmpEq.assert_fields_are_eq
{T : Type} (corecmpEqInst : core.cmp.Eq T) (self : Struct T) :
Result Unit
:= do
Expand All @@ -841,8 +840,8 @@ def Struct.Insts.CoreCmpEq {T : Type} (corecmpEqInst : core.cmp.Eq T) :
core.cmp.Eq (Struct T) := {
partialEqInst := Struct.Insts.CoreCmpPartialEqStruct
corecmpEqInst.partialEqInst
assert_receiver_is_total_eq :=
Struct.Insts.CoreCmpEq.assert_receiver_is_total_eq corecmpEqInst
assert_fields_are_eq := Struct.Insts.CoreCmpEq.assert_fields_are_eq
corecmpEqInst
}

/-- [derive::{impl core::fmt::Debug for derive::Struct<T>}::fmt]:
Expand Down Expand Up @@ -939,10 +938,10 @@ def Struct6Fields.Insts.CoreCmpPartialEqStruct6Fields : core.cmp.PartialEq
ne := Struct6Fields.Insts.CoreCmpPartialEqStruct6Fields.ne
}

/-- [derive::{impl core::cmp::Eq for derive::Struct6Fields}::assert_receiver_is_total_eq]:
/-- [derive::{impl core::cmp::Eq for derive::Struct6Fields}::assert_fields_are_eq]:
Source: 'tests/src/derive.rs', lines 54:27-54:29
Visibility: public -/
def Struct6Fields.Insts.CoreCmpEq.assert_receiver_is_total_eq
def Struct6Fields.Insts.CoreCmpEq.assert_fields_are_eq
(self : Struct6Fields) : Result Unit := do
ok ()

Expand All @@ -951,8 +950,7 @@ def Struct6Fields.Insts.CoreCmpEq.assert_receiver_is_total_eq
@[reducible]
def Struct6Fields.Insts.CoreCmpEq : core.cmp.Eq Struct6Fields := {
partialEqInst := Struct6Fields.Insts.CoreCmpPartialEqStruct6Fields
assert_receiver_is_total_eq :=
Struct6Fields.Insts.CoreCmpEq.assert_receiver_is_total_eq
assert_fields_are_eq := Struct6Fields.Insts.CoreCmpEq.assert_fields_are_eq
}

/-- [derive::{impl core::fmt::Debug for derive::Struct6Fields}::fmt]:
Expand Down
4 changes: 2 additions & 2 deletions tests/lean/Iterators.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -39,7 +39,7 @@ axiom core.iter.adapters.zip.Zip.Insts.CoreIterTraitsIteratorIteratorPair.next
Clause1_Item)) × (core.iter.adapters.zip.Zip A B))

/-- [core::iter::range::{impl core::iter::traits::iterator::Iterator<A> for core::ops::range::Range<A>}::zip]:
Source: '/rustc/library/core/src/iter/range.rs', lines 852:0-852:40
Source: '/rustc/library/core/src/iter/range.rs', lines 980:0-980:40
Name pattern: [core::iter::range::{core::iter::traits::iterator::Iterator<core::ops::range::Range<@A>, @A>}::zip]
Visibility: public -/
@[rust_fun
Expand All @@ -52,7 +52,7 @@ axiom core.ops.range.Range.Insts.CoreIterTraitsIteratorIterator.zip
(core.ops.range.Range A) Clause1_IntoIter)

/-- [core::iter::traits::iterator::Iterator::zip]:
Source: '/rustc/library/core/src/iter/traits/iterator.rs', lines 626:4-629:24
Source: '/rustc/library/core/src/iter/traits/iterator.rs', lines 631:4-634:24
Name pattern: [core::iter::traits::iterator::Iterator::zip]
Visibility: public -/
@[rust_fun "core::iter::traits::iterator::Iterator::zip"]
Expand Down
8 changes: 4 additions & 4 deletions tests/lean/LoopsIssues.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -18,7 +18,7 @@ noncomputable section
namespace loops_issues

/-- [core::iter::range::{impl core::iter::range::Step for i32}::backward_checked]:
Source: '/rustc/library/core/src/iter/range.rs', lines 340:16-340:74
Source: '/rustc/library/core/src/iter/range.rs', lines 342:16-342:74
Name pattern: [core::iter::range::{core::iter::range::Step<i32>}::backward_checked]
Visibility: public -/
@[rust_fun
Expand All @@ -27,7 +27,7 @@ axiom I32.Insts.CoreIterRangeStep.backward_checked
: Std.I32 → Std.Usize → Result (Option Std.I32)

/-- [core::iter::range::{impl core::iter::range::Step for i32}::forward_checked]:
Source: '/rustc/library/core/src/iter/range.rs', lines 319:16-319:73
Source: '/rustc/library/core/src/iter/range.rs', lines 321:16-321:73
Name pattern: [core::iter::range::{core::iter::range::Step<i32>}::forward_checked]
Visibility: public -/
@[rust_fun
Expand All @@ -36,15 +36,15 @@ axiom I32.Insts.CoreIterRangeStep.forward_checked
: Std.I32 → Std.Usize → Result (Option Std.I32)

/-- [core::iter::range::{impl core::iter::range::Step for i32}::steps_between]:
Source: '/rustc/library/core/src/iter/range.rs', lines 304:16-304:84
Source: '/rustc/library/core/src/iter/range.rs', lines 306:16-306:84
Name pattern: [core::iter::range::{core::iter::range::Step<i32>}::steps_between]
Visibility: public -/
@[rust_fun "core::iter::range::{core::iter::range::Step<i32>}::steps_between"]
axiom I32.Insts.CoreIterRangeStep.steps_between
: Std.I32 → Std.I32 → Result (Std.Usize × (Option Std.Usize))

/-- Trait implementation: [core::iter::range::{impl core::iter::range::Step for i32}]
Source: '/rustc/library/core/src/iter/range.rs', lines 299:12-299:37
Source: '/rustc/library/core/src/iter/range.rs', lines 301:12-301:43
Name pattern: [core::iter::range::Step<i32>] -/
@[reducible, rust_trait_impl "core::iter::range::Step<i32>"]
def I32.Insts.CoreIterRangeStep : core.iter.range.Step Std.I32 := {
Expand Down
Loading
Loading