Skip to content

Format Lean 4 generated code #4747

Open
Open
Format Lean 4 generated code#4747
Labels
lean4-backend

Description

@JuanCoRo
JuanCoRo
opened on Jan 24, 2025

We should format the generated Lean 4 code according to some standard. Perhaps by piping it to an external formatter.

Activity

  1. JuanCoRo
    added
    lean4-backend
    on Jan 24, 2025
  2. JuanCoRo
    changed the title [-]Format Lean 4 produce code[/-] [+]Format Lean 4 generated code[/+] on Jan 24, 2025

  3. JuanCoRo commented on Jan 31, 2025

    @JuanCoRo
    JuanCoRo
    on Jan 31, 2025
    MemberAuthor

    See here for documentation on lean lint

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Metadata

Metadata

Assignees

No one assigned

    Labels

    lean4-backend

    Type

    No type

    Projects

    No projects

      Milestone

      No milestone

      Relationships

      None yet

      Development

      No branches or pull requests

      Issue actions