Skip to content

Add set_option pp.unicode false #1056

@leodemoura

Description

@leodemoura

We had this option in Lean 3.

Metadata

Metadata

Assignees

No one assigned

    Labels

    P-mediumWe may work on this issue if we find the timeenhancementNew feature or requestlean4_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