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

feat(script/gen_constants_cpp.py): support for provifing custom C name

Browse Source
This commit is contained in:
Leonardo de Moura
2019-03-20 17:51:48 -07:00
parent 79a8d9aa65
commit d78ad40aaf
1 changed files with 5 additions and 1 deletions
Download Patch File Download Diff File Expand all files Collapse all files

6
script/gen_constants_cpp.py
View File

@@ -47,7 +47,11 @@ def main(argv=None):
constants = []
with open(infile, 'r') as f:
for line in f:
constants.append([to_c_const(line.strip()), line.strip()])
p = line.split()
if len(p) == 2:
constants.append([p[1].strip(), p[0].strip()])
else:
constants.append([to_c_const(line.strip()), line.strip()])
basedir, name = os.path.split(infile)
os.chdir(basedir)