max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore(bin/lean-gdb): remove lean::name from string output

Browse source
This commit is contained in:
Gabriel Ebner 2016-11-07 14:21:39 -05:00 • committed by Leonardo de Moura
parent dad7de5578
commit 38ee100117
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
bin/lean-gdb.py
View file

@ -16,9 +16,9 @@ class LeanNamePrinter:
return s
if not self.val['m_ptr']:
return "lean::name()"
return ""
else:
return 'lean::name(%s)' % rec(self.val['m_ptr'].dereference())
return rec(self.val['m_ptr'].dereference())
class LeanListPrinter:
"""Print a lean::list object."""