Add set_option pp.unicode false #1056

New issue

Copy link

New issue

Copy link

Closed

#10384

Closed

Add set_option pp.unicode false#1056

#10384

Copy link

Labels

P-mediumWe may work on this issue if we find the timeWe may work on this issue if we find the timeenhancementNew feature or requestNew feature or requestlean4_releaseMust be addressed before first official releaseMust be addressed before first official release

Description

leodemoura

opened on Mar 20, 2022

Issue body actions

We had this option in Lean 3.

Reactions are currently unavailable

Metadata

Metadata

Assignees

No one assigned

Labels

P-mediumWe may work on this issue if we find the timeWe may work on this issue if we find the timeenhancementNew feature or requestNew feature or requestlean4_releaseMust be addressed before first official releaseMust be addressed before first official release

Type

No type

Projects

No projects

Milestone

No milestone

Relationships

None yet

Development

No branches or pull requests

Issue actions