| /- | |
| Copyright (c) 2021 Microsoft Corporation. All rights reserved. | |
| Released under Apache 2.0 license as described in the file LICENSE. | |
| Authors: Leonardo de Moura | |
| -/ | |
| import Lean.MonadEnv | |
| namespace Lean | |
| builtin_initialize docStringExt : MapDeclarationExtension String ← mkMapDeclarationExtension `docstring | |
| def addDocString [MonadEnv m] (declName : Name) (docString : String) : m Unit := | |
| modifyEnv fun env => docStringExt.insert env declName docString | |
| def addDocString' [Monad m] [MonadEnv m] (declName : Name) (docString? : Option String) : m Unit := | |
| match docString? with | |
| | some docString => addDocString declName docString | |
| | none => return () | |
| def findDocString? [Monad m] [MonadEnv m] (declName : Name) : m (Option String) := | |
| return docStringExt.find? (← getEnv) declName | |
| end Lean |