From 90dc3356dc872fb22ee5f99cd609e2adf65dcc86 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 3 Jun 2019 16:24:36 -0700 Subject: [PATCH] chore(library/init/lean/environment): remove unnecessary local instance --- library/init/lean/environment.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/library/init/lean/environment.lean b/library/init/lean/environment.lean index dfa5617410..12ba979a82 100644 --- a/library/init/lean/environment.lean +++ b/library/init/lean/environment.lean @@ -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. -/