summaryrefslogtreecommitdiff
path: root/backends/lean/Base/Primitives/Alloc.lean
blob: 15fe1ff9ec13322c637ba09565b3d15ec9d0c1fe (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
import Lean
import Base.Primitives.Base
import Base.Primitives.CoreOps

open Primitives
open Result

namespace alloc

namespace boxed -- alloc.boxed

namespace Box -- alloc.boxed.Box

def deref (T : Type) (x : T) : Result T := ok x
def deref_mut (T : Type) (x : T) : Result (T × (T  Result T)) := ok (x, λ x => ok 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
}

end Box -- alloc.boxed.Box

end boxed -- alloc.boxed

end alloc