blob: aa4a7f285d907393fee1db41c7bcd8cd141bfbfc (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
|
import Lean
import Base.Primitives.Base
open Primitives
open Result
namespace core
/- Trait declaration: [core::convert::From] -/
structure convert.From (Self T : Type) where
from_ : T → Result Self
namespace ops -- core.ops
namespace index -- core.ops.index
/- Trait declaration: [core::ops::index::Index] -/
structure Index (Self Idx : Type) where
Output : Type
index : Self → Idx → Result Output
/- Trait declaration: [core::ops::index::IndexMut] -/
structure IndexMut (Self Idx : Type) where
indexInst : Index Self Idx
index_mut : Self → Idx → Result (indexInst.Output × (indexInst.Output → Result Self))
end index -- core.ops.index
namespace deref -- core.ops.deref
structure Deref (Self : Type) where
Target : Type
deref : Self → Result Target
structure DerefMut (Self : Type) where
derefInst : Deref Self
deref_mut : Self → Result (derefInst.Target × (Self → Result Self))
end deref -- core.ops.deref
end ops -- core.ops
/- Trait declaration: [core::clone::Clone] -/
structure clone.Clone (Self : Type) where
clone : Self → Result Self
/- [core::clone::impls::{(core::clone::Clone for bool)#19}::clone] -/
def clone.impls.CloneBool.clone (b : Bool) : Bool := b
def clone.CloneBool : clone.Clone Bool := {
clone := fun b => ok (clone.impls.CloneBool.clone b)
}
namespace option -- core.option
/- [core::option::{core::option::Option<T>}::unwrap] -/
def Option.unwrap (T : Type) (x : Option T) : Result T :=
Result.ofOption x Error.panic
end option -- core.option
/- [core::option::Option::take] -/
@[simp] def Option.take (T: Type) (self: Option T): Option T × Option T := (self, .none)
/- [core::mem::replace]
This acts like a swap effectively in a functional pure world.
We return the old value of `dst`, i.e. `dst` itself.
The new value of `dst` is `src`. -/
@[simp] def mem.replace (a : Type) (dst : a) (src : a) : a × a := (dst, src)
/- [core::mem::swap] -/
@[simp] def mem.swap (T: Type) (a b: T): T × T := (b, a)
end core
|
