diff options
| author | Son Ho | 2023-12-05 17:34:13 +0100 |
|---|---|---|
| committer | Son Ho | 2023-12-05 17:34:13 +0100 |
| commit | 726db4911add81a853aafcec3936b457aaeff5b4 (patch) | |
| tree | 2663915767c3558203990ed14f8d5604b7fd21d1 /tests/lean/External/FunsExternal_Template.lean | |
| parent | 92887b89e35607e99bae2f19e4c5b2f162683d02 (diff) | |
| parent | 4795e5f823bc89504855d8eb946b111d9314f4d5 (diff) | |
Merge branch 'main' into son_fixes2
Diffstat (limited to '')
| -rw-r--r-- | tests/lean/External/FunsExternal_Template.lean | 15 |
1 files changed, 10 insertions, 5 deletions
diff --git a/tests/lean/External/FunsExternal_Template.lean b/tests/lean/External/FunsExternal_Template.lean index c8bc397f..55cd6bb5 100644 --- a/tests/lean/External/FunsExternal_Template.lean +++ b/tests/lean/External/FunsExternal_Template.lean @@ -6,22 +6,27 @@ import External.Types open Primitives open external -/- [core::mem::swap]: forward function -/ +/- [core::mem::swap]: forward function + Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/mem/mod.rs', lines 726:0-726:42 -/ axiom core.mem.swap (T : Type) : T → T → State → Result (State × Unit) -/- [core::mem::swap]: backward function 0 -/ +/- [core::mem::swap]: backward function 0 + Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/mem/mod.rs', lines 726:0-726:42 -/ axiom core.mem.swap_back0 (T : Type) : T → T → State → State → Result (State × T) -/- [core::mem::swap]: backward function 1 -/ +/- [core::mem::swap]: backward function 1 + Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/mem/mod.rs', lines 726:0-726:42 -/ axiom core.mem.swap_back1 (T : Type) : T → T → State → State → Result (State × T) -/- [core::num::nonzero::NonZeroU32::{14}::new]: forward function -/ +/- [core::num::nonzero::{core::num::nonzero::NonZeroU32#14}::new]: forward function + Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/num/nonzero.rs', lines 79:16-79:57 -/ axiom core.num.nonzero.NonZeroU32.new : U32 → State → Result (State × (Option core.num.nonzero.NonZeroU32)) -/- [core::option::Option::{0}::unwrap]: forward function -/ +/- [core::option::{core::option::Option<T>}::unwrap]: forward function + Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/option.rs', lines 932:4-932:34 -/ axiom core.option.Option.unwrap (T : Type) : Option T → State → Result (State × T) |