sdgoij/lean4
1
0
Fork 0
mirror of https://github.com/leanprover/lean4.git synced 2026-03-17 18:34:06 +00:00
Code Issues Packages Projects Releases Wiki Activity

refactor(library/system/io): move into init

Browse Source
This commit is contained in:
Sebastian Ullrich
2018-08-15 09:43:48 -07:00
committed by Leonardo de Moura
parent a260bf91d4
commit 37e5f03351
13 changed files with 12 additions and 12 deletions
Download Patch File Download Diff File Expand all files Collapse all files

2
script/gen_constants_cpp.py
View File

@@ -90,7 +90,7 @@ def main(argv=None):
return 0
with open(tst_file, 'w') as f:
f.write('-- DO NOT EDIT, automatically generated file, generator scripts/gen_constants_cpp.py\n')
f.write("import system.io\n")
f.write("import init.io\n")
f.write("open tactic\n");
f.write("meta def script_check_id (n : name) : tactic unit :=\n");
f.write("do env ← get_env, (env^.get n >> return ()) <|> (guard $ env^.is_namespace n) <|> (attribute.get_instances n >> return ()) <|> fail (\"identifier '\" ++ to_string n ++ \"' is not a constant, namespace nor attribute\")\n");