Skip to content
This repository was archived by the owner on Aug 24, 2024. It is now read-only.
This repository was archived by the owner on Aug 24, 2024. It is now read-only.

We need to get back the "Copy to clipboard" button on Lean code snippets  #35

Description

@lovettchris

Description

Copy/paste the output of Alectryon on lean code snippets produces a big mess in your VS code text editor.

Detailed behaviour

Go to https://leanprover.github.io/lean4/doc/monads/functors.lean.html and select the first lean snippet for List.map and paste it into VS code and you will get this:

#eval
["1", "2", "3"]

List.map (λ
x =>
toString
x) [
1,
2,
3] -- ["1", "2", "3"]

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Fields

    No fields configured for issues without a type.

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions