fix: universe commands in environment capture #183

Merged
aniva merged 5 commits from bug/variable-level-names-in-scope into dev 2025-04-07 20:18:50 -07:00
1 changed files with 1 additions and 1 deletions
Showing only changes of commit 9216e4fa86 - Show all commits

View File

@ -180,7 +180,7 @@ def addDecl (name: String) (levels: Array String := #[]) (type?: Option String)
Lean.Declaration.thmDecl <| Lean.mkTheoremValEx
(name := name.toName)
(levelParams := levelParams)
(type := type )
(type := type)
(value := value)
(all := [])
else