96f9ee2a41
This PR ensures info tree users such as linters and request handlers have access to info subtrees created by async elab task by introducing API to leave holes filled by such tasks. **Breaking change**: other metaprogramming users of `Command.State.infoState` may need to call `InfoState.substituteLazy` on it manually to fill all holes.
43 lines
922 B
Text
43 lines
922 B
Text
/-
|
|
Copyright (c) 2014 Microsoft Corporation. All rights reserved.
|
|
Released under Apache 2.0 license as described in the file LICENSE.
|
|
Authors: Leonardo de Moura
|
|
-/
|
|
prelude
|
|
import Init.Prelude
|
|
import Init.Notation
|
|
import Init.Tactics
|
|
import Init.TacticsExtra
|
|
import Init.ByCases
|
|
import Init.RCases
|
|
import Init.Core
|
|
import Init.Control
|
|
import Init.Data.Basic
|
|
import Init.WF
|
|
import Init.WFTactics
|
|
import Init.Data
|
|
import Init.System
|
|
import Init.Util
|
|
import Init.Dynamic
|
|
import Init.ShareCommon
|
|
import Init.MetaTypes
|
|
import Init.Meta
|
|
import Init.NotationExtra
|
|
import Init.SimpLemmas
|
|
import Init.PropLemmas
|
|
import Init.Hints
|
|
import Init.Conv
|
|
import Init.Guard
|
|
import Init.Simproc
|
|
import Init.SizeOfLemmas
|
|
import Init.BinderPredicates
|
|
import Init.Ext
|
|
import Init.Omega
|
|
import Init.MacroTrace
|
|
import Init.Grind
|
|
import Init.While
|
|
import Init.Syntax
|
|
import Init.Internal
|
|
import Init.Try
|
|
import Init.BinderNameHint
|
|
import Init.Task
|