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

chore: missing prelude

Browse source
This commit is contained in:
Leonardo de Moura 2024-02-25 11:03:55 -08:00 • committed by Leonardo de Moura
parent b9b7f97d42
commit 88fbe2e531
4 changed files with 4 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/Lean/Elab/GuardMsgs.lean
View file

@ -3,6 +3,7 @@ Copyright (c) 2023 Kyle Miller. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Kyle Miller
-/
prelude
import Lean.Server.CodeActions.Attr
/-! `#guard_msgs` command for testing commands

1
src/Lean/Server/CodeActions.lean
View file

@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
Authors: E.W.Ayers
-/
prelude
import Lean.Server.CodeActions.Attr
import Lean.Server.CodeActions.Basic
import Lean.Server.CodeActions.Provider

1
src/Lean/Server/CodeActions/Attr.lean
View file

@ -3,6 +3,7 @@ Copyright (c) 2023 Mario Carneiro. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Mario Carneiro
-/
prelude
import Lean.Server.CodeActions.Basic
/-!

1
src/Lean/Server/CodeActions/Provider.lean
View file

@ -3,6 +3,7 @@ Copyright (c) 2023 Mario Carneiro. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Mario Carneiro
-/
prelude
import Lean.Elab.BuiltinTerm
import Lean.Elab.BuiltinNotation
import Lean.Server.InfoUtils