summaryrefslogtreecommitdiff
path: root/tests/lean/External/FunsExternal.lean
blob: 28ba2077dc5718f8c6af84baeea3b8182e8ce718 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
-- [external]: templates for the external functions.
import Base
import External.Types
open Primitives
open external

/- [core::cell::{core::cell::Cell<T>#10}::get]: -/
def core.cell.Cell.get
  (T : Type) (markerCopyInst : core.marker.Copy T) (c : core.cell.Cell T) (s : State) :
  Result (State × T) :=
  sorry

/- [core::cell::{core::cell::Cell<T>#11}::get_mut]: -/
def core.cell.Cell.get_mut (T : Type) (c : core.cell.Cell T) (s : State) :
  Result (State × (T × (T  State  Result (State × (core.cell.Cell T))))) :=
  sorry