lean4-htt/tests/lean/interactive/projects/InverseModuleHierarchy/InverseModuleHierarchy/BasicTest.lean.disabled

6 lines
79 B
Text

def hello := "world"
#eval 1
--^ waitForILeans
--^ moduleHierarchyImportedBy