Std.ShareCommon

source

@[inline]

abbrev Std.ShareCommon.Object :

Type

Equations

Std.ShareCommon.Object = NonScalar

source

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

Bool

Equations

Std.ShareCommon.Object.ptrEq a b = (ptrAddrUnsafe a == ptrAddrUnsafe b)

source

@[inline]

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

UInt64

Equations

Std.ShareCommon.Object.ptrHash a = USize.toUInt64 (ptrAddrUnsafe a)

source

@[extern lean_sharecommon_eq]

unsafe constant Std.ShareCommon.Object.eq (a : Std.ShareCommon.Object) (b : Std.ShareCommon.Object) :

Bool

source

@[extern lean_sharecommon_hash]

unsafe constant Std.ShareCommon.Object.hash (a : Std.ShareCommon.Object) :

UInt64

source

unsafe noncomputable def Std.ShareCommon.ObjectMap :

Type

Equations

Std.ShareCommon.ObjectMap = Std.HashMap Std.ShareCommon.Object Std.ShareCommon.Object

source

unsafe noncomputable def Std.ShareCommon.ObjectSet :

Type

Equations

Std.ShareCommon.ObjectSet = Std.HashSet Std.ShareCommon.Object

source

unsafe noncomputable def Std.ShareCommon.ObjectPersistentMap :

Type

Equations

Std.ShareCommon.ObjectPersistentMap = Std.PersistentHashMap Std.ShareCommon.Object Std.ShareCommon.Object

source

unsafe noncomputable def Std.ShareCommon.ObjectPersistentSet :

Type

Equations

Std.ShareCommon.ObjectPersistentSet = Std.PersistentHashSet Std.ShareCommon.Object

source

unsafe def Std.ShareCommon.mkObjectMap :

Unit → Std.ShareCommon.ObjectMap

Equations

Std.ShareCommon.mkObjectMap x = Std.mkHashMap 1024

source

unsafe def Std.ShareCommon.ObjectMap.find? (m : Std.ShareCommon.ObjectMap) (k : Std.ShareCommon.Object) :

Option Std.ShareCommon.Object

Equations

Std.ShareCommon.ObjectMap.find? m k = Std.HashMap.find? m k

source

unsafe def Std.ShareCommon.ObjectMap.insert (m : Std.ShareCommon.ObjectMap) (k : Std.ShareCommon.Object) (v : Std.ShareCommon.Object) :

Std.ShareCommon.ObjectMap

Equations

Std.ShareCommon.ObjectMap.insert m k v = Std.HashMap.insert m k v

source

unsafe def Std.ShareCommon.mkObjectSet :

Unit → Std.ShareCommon.ObjectSet

Equations

Std.ShareCommon.mkObjectSet x = Std.mkHashSet 1024

source

unsafe def Std.ShareCommon.ObjectSet.find? (s : Std.ShareCommon.ObjectSet) (o : Std.ShareCommon.Object) :

Option Std.ShareCommon.Object

Equations

Std.ShareCommon.ObjectSet.find? s o = Std.HashSet.find? s o

source

unsafe def Std.ShareCommon.ObjectSet.insert (s : Std.ShareCommon.ObjectSet) (o : Std.ShareCommon.Object) :

Std.ShareCommon.ObjectSet

Equations

Std.ShareCommon.ObjectSet.insert s o = Std.HashSet.insert s o

source

unsafe def Std.ShareCommon.mkObjectPersistentMap :

Unit → Std.ShareCommon.ObjectPersistentMap

Equations

Std.ShareCommon.mkObjectPersistentMap x = Std.PersistentHashMap.empty

source

unsafe def Std.ShareCommon.ObjectPersistentMap.find? (m : Std.ShareCommon.ObjectPersistentMap) (k : Std.ShareCommon.Object) :

Option Std.ShareCommon.Object

Equations

Std.ShareCommon.ObjectPersistentMap.find? m k = Std.PersistentHashMap.find? m k

source

unsafe def Std.ShareCommon.ObjectPersistentMap.insert (m : Std.ShareCommon.ObjectPersistentMap) (k : Std.ShareCommon.Object) (v : Std.ShareCommon.Object) :

Std.ShareCommon.ObjectPersistentMap

Equations

Std.ShareCommon.ObjectPersistentMap.insert m k v = Std.PersistentHashMap.insert m k v

source

unsafe def Std.ShareCommon.mkObjectPersistentSet :

Unit → Std.ShareCommon.ObjectPersistentSet

Equations

Std.ShareCommon.mkObjectPersistentSet x = Std.PersistentHashSet.empty

source

unsafe def Std.ShareCommon.ObjectPersistentSet.find? (s : Std.ShareCommon.ObjectPersistentSet) (o : Std.ShareCommon.Object) :

Option Std.ShareCommon.Object

Equations

Std.ShareCommon.ObjectPersistentSet.find? s o = Std.PersistentHashSet.find? s o

source

unsafe def Std.ShareCommon.ObjectPersistentSet.insert (s : Std.ShareCommon.ObjectPersistentSet) (o : Std.ShareCommon.Object) :

Std.ShareCommon.ObjectPersistentSet

Equations

Std.ShareCommon.ObjectPersistentSet.insert s o = Std.PersistentHashSet.insert s o

source

constant Std.ShareCommon.StatePointed :

NonemptyType

source

@[inline]

abbrev Std.ShareCommon.State :

Type u

Equations

Std.ShareCommon.State = NonemptyType.type Std.ShareCommon.StatePointed

source

@[extern lean_sharecommon_mk_state]

constant Std.ShareCommon.mkState :

Unit → Std.ShareCommon.State

source

def Std.ShareCommon.State.empty :

Std.ShareCommon.State

Equations

Std.ShareCommon.State.empty = Std.ShareCommon.mkState ()

source

instance Std.ShareCommon.State.inhabited :

Inhabited Std.ShareCommon.State

Equations

Std.ShareCommon.State.inhabited = { default := Std.ShareCommon.State.empty }

source

constant Std.ShareCommon.PersistentStatePointed :

NonemptyType

source

@[inline]

abbrev Std.ShareCommon.PersistentState :

Type u

Equations

Std.ShareCommon.PersistentState = NonemptyType.type Std.ShareCommon.PersistentStatePointed

source

@[extern lean_sharecommon_mk_pstate]

constant Std.ShareCommon.mkPersistentState :

Unit → Std.ShareCommon.PersistentState

source

def Std.ShareCommon.PersistentState.empty :

Std.ShareCommon.PersistentState

Equations

Std.ShareCommon.PersistentState.empty = Std.ShareCommon.mkPersistentState ()

source

instance Std.ShareCommon.PersistentState.inhabited :

Inhabited Std.ShareCommon.PersistentState

Equations

Std.ShareCommon.PersistentState.inhabited = { default := Std.ShareCommon.PersistentState.empty }

source

@[inline]

abbrev Std.ShareCommon.PState :

Type u

Equations

Std.ShareCommon.PState = Std.ShareCommon.PersistentState

source

@[extern lean_state_sharecommon]

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

α × Std.ShareCommon.State

Equations

Std.ShareCommon.State.shareCommon s a = (a, s)

source

@[extern lean_persistent_state_sharecommon]

def Std.ShareCommon.PersistentState.shareCommon {α : Type u_1} (s : Std.ShareCommon.PersistentState) (a : α) :

α × Std.ShareCommon.PersistentState

Equations

Std.ShareCommon.PersistentState.shareCommon s a = (a, s)

source

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

Type (max (u + 1) v)

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

Instances

source

@[inline]

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

α → m α

Equations

@Std.withShareCommon = @Std.MonadShareCommon.withShareCommon

source

@[inline]

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

m α

Equations

Std.shareCommonM a = Std.withShareCommon a

source

@[inline]

abbrev Std.ShareCommonT (m : Type u → Type v) (α : Type u) :

Type (max u v)

Equations

Std.ShareCommonT m = StateT Std.ShareCommon.State m

source

@[inline]

abbrev Std.PShareCommonT (m : Type u → Type v) (α : Type u) :

Type (max u v)

Equations

Std.PShareCommonT m = StateT Std.ShareCommon.PState m

source

@[inline]

abbrev Std.ShareCommonM (α : Type u_1) :

Type u_1

Equations

Std.ShareCommonM = Std.ShareCommonT Id

source

@[inline]

abbrev Std.PShareCommonM (α : Type u_1) :

Type u_1

Equations

Std.PShareCommonM = Std.PShareCommonT Id

source

@[specialize]

def Std.ShareCommonT.withShareCommon {m : Type u_1 → Type u_2} {α : Type u_1} [inst : Monad m] (a : α) :

Std.ShareCommonT m α

Equations

Std.ShareCommonT.withShareCommon a = modifyGet fun s => Std.ShareCommon.State.shareCommon s a

source

@[specialize]

def Std.PShareCommonT.withShareCommon {m : Type u_1 → Type u_2} {α : Type u_1} [inst : Monad m] (a : α) :

Std.PShareCommonT m α

Equations

Std.PShareCommonT.withShareCommon a = modifyGet fun s => Std.ShareCommon.PersistentState.shareCommon s a

source

instance Std.ShareCommonT.monadShareCommon {m : Type u_1 → Type u_2} [inst : Monad m] :

Std.MonadShareCommon (Std.ShareCommonT m)

Equations

Std.ShareCommonT.monadShareCommon = { withShareCommon := fun {α} => Std.ShareCommonT.withShareCommon }

source

instance Std.PShareCommonT.monadShareCommon {m : Type u_1 → Type u_2} [inst : Monad m] :

Std.MonadShareCommon (Std.PShareCommonT m)

Equations

Std.PShareCommonT.monadShareCommon = { withShareCommon := fun {α} => Std.PShareCommonT.withShareCommon }

source

@[inline]

def Std.ShareCommonT.run {m : Type u_1 → Type u_2} {α : Type u_1} [inst : Monad m] (x : Std.ShareCommonT m α) :

m α

Equations

Std.ShareCommonT.run x = StateT.run' x Std.ShareCommon.State.empty

source

@[inline]

def Std.PShareCommonT.run {m : Type u_1 → Type u_2} {α : Type u_1} [inst : Monad m] (x : Std.PShareCommonT m α) :

m α

Equations

Std.PShareCommonT.run x = StateT.run' x Std.ShareCommon.PersistentState.empty

source

@[inline]

def Std.ShareCommonM.run {α : Type u_1} (x : Std.ShareCommonM α) :

α

Equations

Std.ShareCommonM.run x = Std.ShareCommonT.run x

source

@[inline]

def Std.PShareCommonM.run {α : Type u_1} (x : Std.PShareCommonM α) :

α

Equations

Std.PShareCommonM.run x = Std.PShareCommonT.run x

source

def Std.shareCommon {α : Type u_1} (a : α) :

α

Equations

Std.shareCommon a = Std.ShareCommonM.run (Std.withShareCommon a)