blob: 0580421f0e7468fae45c27dd787ea0fdeaedf0e5 (
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
|
import Lean
import Base.Primitives.Base
import Base.Primitives.CoreOpsDeref
open Primitives
open Result
namespace alloc
namespace boxed -- alloc.boxed
namespace Box -- alloc.boxed.Box
def deref (T : Type) (x : T) : Result T := ret x
def deref_mut (T : Type) (x : T) : Result T := ret x
def deref_mut_back (T : Type) (_ : T) (x : T) : Result T := ret x
/-- Trait instance -/
def coreOpsDerefInst (Self : Type) :
core.ops.deref.Deref Self := {
Target := Self
deref := deref Self
}
/-- Trait instance -/
def coreOpsDerefMutInst (Self : Type) :
core.ops.deref.DerefMut Self := {
derefInst := coreOpsDerefInst Self
deref_mut := deref_mut Self
deref_mut_back := deref_mut_back Self
}
end Box -- alloc.boxed.Box
end boxed -- alloc.boxed
end alloc
|
