chore: Focus on basic declarations for now

main
Henrik Böving 2021-12-04 22:32:34 +01:00
parent ac8d9e254e
commit b8cf967b84
1 changed files with 0 additions and 1 deletions

View File

@ -64,7 +64,6 @@ inductive DocInfo where
| inductiveInfo (info : InductiveInfo) : DocInfo | inductiveInfo (info : InductiveInfo) : DocInfo
| structureInfo (info : StructureInfo) : DocInfo | structureInfo (info : StructureInfo) : DocInfo
| classInfo (info : ClassInfo) : DocInfo | classInfo (info : ClassInfo) : DocInfo
| classInductiveInfo : DocInfo
structure Module where structure Module where
name : Name name : Name