mathport icon indicating copy to clipboard operation
mathport copied to clipboard
verified publisher icon leanprover-community

feat: lightweight support for optional pp in raw tactic state

Open dselsam opened this issue 4 years ago • 0 comments

lighter-weight alternative to https://github.com/leanprover-community/mathport/pull/136 consistent with the changed export format in https://github.com/leanprover-community/lean/pull/702/commits/a8b8424c6dd64e2135661c6a580a397c3663b2e8

dselsam avatar Mar 17 '22 21:03 dselsam