max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore(library/init/lean/environment): remove unnecessary local instance

Browse source
This commit is contained in:
Leonardo de Moura 2019-06-03 16:24:36 -07:00
parent 4a26f0028c
commit 90dc3356dc
1 changed files with 3 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
library/init/lean/environment.lean
View file

@ -223,14 +223,14 @@ IO.mkRef Array.empty
@[init mkPersistentEnvExtensionsRef]
private constant persistentEnvExtensionsRef : IO.Ref (Array (PersistentEnvExtension EnvExtensionEntry EnvExtensionState)) := default _
structure PersistentEnvExtensionDescr (α σ : Type) [Inhabited α] :=
structure PersistentEnvExtensionDescr (α σ : Type) :=
(name : Name)
(initState : σ)
(addEntryFn : Bool → σ → α → σ)
(toArrayFn : List α → Array α := λ as, as.toArray)
(lazy := true)
unsafe def registerPersistentEnvExtensionUnsafe {α σ : Type} [Inhabited α] (descr : PersistentEnvExtensionDescr α σ) : IO (PersistentEnvExtension α σ) :=
unsafe def registerPersistentEnvExtensionUnsafe {α σ : Type} (descr : PersistentEnvExtensionDescr α σ) : IO (PersistentEnvExtension α σ) :=
do
let s : PersistentEnvExtensionState α σ := {
importedEntries := Array.empty,
@ -251,7 +251,7 @@ persistentEnvExtensionsRef.modify (λ pExts, pExts.push (unsafeCast pExt)),
pure pExt
@[implementedBy registerPersistentEnvExtensionUnsafe]
constant registerPersistentEnvExtension {α σ : Type} [Inhabited α] (descr : PersistentEnvExtensionDescr α σ) : IO (PersistentEnvExtension α σ) := default _
constant registerPersistentEnvExtension {α σ : Type} (descr : PersistentEnvExtensionDescr α σ) : IO (PersistentEnvExtension α σ) := default _
/- API for creating extensions in C++.
This API will eventually be deleted. -/