Init.ShareCommon

source

@[inline, reducible]

abbrev ShareCommon.Object :

Type

Instances For

source

unsafe def ShareCommon.Object.ptrEq (a : ShareCommon.Object) (b : ShareCommon.Object) :

Bool

Instances For

source

@[inline, reducible]

unsafe abbrev ShareCommon.Object.ptrHash (a : ShareCommon.Object) :

UInt64

Instances For

source

structure ShareCommon.StateFactoryImpl :

Type 1

Map : Type
Set : Type
mkState : Unit → s.Map × s.Set
mapFind? : s.Map → ShareCommon.Object → Option ShareCommon.Object
mapInsert : s.Map → ShareCommon.Object → ShareCommon.Object → s.Map
setFind? : s.Set → ShareCommon.Object → Option ShareCommon.Object
setInsert : s.Set → ShareCommon.Object → s.Set

Instances For

source

opaque ShareCommon.StateFactoryPointed :

NonemptyType

source

@[inline, reducible]

abbrev ShareCommon.StateFactory :

Type

Instances For

source

instance ShareCommon.instNonemptyStateFactory :

Nonempty ShareCommon.StateFactory

source

@[extern lean_sharecommon_eq]

unsafe opaque ShareCommon.Object.eq (a : ShareCommon.Object) (b : ShareCommon.Object) :

Bool

source

@[extern lean_sharecommon_hash]

unsafe opaque ShareCommon.Object.hash (a : ShareCommon.Object) :

UInt64

source

structure ShareCommon.StateFactoryBuilder :

Type 1

Map : (α : Type) → Type → [inst : BEq α] → [inst : Hashable α] → Type
mkMap : {α β : Type} → [inst : BEq α] → [inst_1 : Hashable α] → Nat → ShareCommon.StateFactoryBuilder.Map s α β
mapFind? : {α β : Type} → [inst : BEq α] → [inst_1 : Hashable α] → ShareCommon.StateFactoryBuilder.Map s α β → α → Option β
mapInsert : {α β : Type} → [inst : BEq α] → [inst_1 : Hashable α] → ShareCommon.StateFactoryBuilder.Map s α β → α → β → ShareCommon.StateFactoryBuilder.Map s α β
Set : (α : Type) → [inst : BEq α] → [inst : Hashable α] → Type
mkSet : {α : Type} → [inst : BEq α] → [inst_1 : Hashable α] → Nat → ShareCommon.StateFactoryBuilder.Set s α
setFind? : {α : Type} → [inst : BEq α] → [inst_1 : Hashable α] → ShareCommon.StateFactoryBuilder.Set s α → α → Option α
setInsert : {α : Type} → [inst : BEq α] → [inst_1 : Hashable α] → ShareCommon.StateFactoryBuilder.Set s α → α → ShareCommon.StateFactoryBuilder.Set s α

Instances For

source

unsafe def ShareCommon.StateFactory.mkImpl :

ShareCommon.StateFactoryBuilder → ShareCommon.StateFactory

Instances For

source

@[implemented_by ShareCommon.StateFactory.mkImpl]

opaque ShareCommon.StateFactory.mk :

ShareCommon.StateFactoryBuilder → ShareCommon.StateFactory

source

unsafe def ShareCommon.StateFactory.get :

ShareCommon.StateFactory → ShareCommon.StateFactoryImpl

Instances For

source

opaque ShareCommon.StatePointed (σ : ShareCommon.StateFactory) :

NonemptyType

Internally State is implemented as a pair ObjectMap and ObjectSet

source

@[inline, reducible]

abbrev ShareCommon.State (σ : ShareCommon.StateFactory) :

Type u

Instances For

source

instance ShareCommon.instNonemptyState {σ : ShareCommon.StateFactory} :

Nonempty (ShareCommon.State σ)

source

unsafe def ShareCommon.mkStateImpl (σ : ShareCommon.StateFactory) :

ShareCommon.State σ

Instances For

source

@[implemented_by ShareCommon.mkStateImpl]

opaque ShareCommon.State.mk (σ : ShareCommon.StateFactory) :

ShareCommon.State σ

source

instance ShareCommon.instInhabitedState {σ : ShareCommon.StateFactory} :

Inhabited (ShareCommon.State σ)

source

@[extern lean_state_sharecommon]

def ShareCommon.State.shareCommon {α : Type u_1} {σ : ShareCommon.StateFactory} (s : ShareCommon.State σ) (a : α) :

α × ShareCommon.State σ

Instances For

source

class MonadShareCommon (m : Type u → Type v) :

Type (max (u + 1) v)

withShareCommon : {α : Type u} → α → m α

Instances

source

@[inline, reducible]

abbrev withShareCommon {m : Type u_1 → Type u_2} [self : MonadShareCommon m] {α : Type u_1} :

α → m α

Instances For

source

@[inline, reducible]

abbrev shareCommonM {m : Type u_1 → Type u_2} {α : Type u_1} [MonadShareCommon m] (a : α) :

m α

Instances For

source

@[inline, reducible]

abbrev ShareCommonT (σ : ShareCommon.StateFactory) (m : Type u → Type v) (α : Type u) :

Type (max u v)

Instances For

source

@[inline, reducible]

abbrev ShareCommonM (σ : ShareCommon.StateFactory) (α : Type u_1) :

Type u_1

Instances For

source

@[specialize #[]]

def ShareCommonT.withShareCommon {m : Type u_1 → Type u_2} {α : Type u_1} {σ : ShareCommon.StateFactory} [Monad m] (a : α) :

ShareCommonT σ m α

Instances For

source

instance ShareCommonT.monadShareCommon {m : Type u_1 → Type u_2} {σ : ShareCommon.StateFactory} [Monad m] :

MonadShareCommon (ShareCommonT σ m)

source

@[inline]

def ShareCommonT.run {m : Type u_1 → Type u_2} {σ : ShareCommon.StateFactory} {α : Type u_1} [Monad m] (x : ShareCommonT σ m α) :

m α

Instances For

source

@[inline]

def ShareCommonM.run {σ : ShareCommon.StateFactory} {α : Type u_1} (x : ShareCommonM σ α) :

Instances For