Skip to content

Plus is used instead Add class #291

Description

@yaitskov

Section says that type should have an instance of class Plus to benefit from operator + though the correct class name for this operator is Add.

Please quote the text that is incorrect:

n the following type class declaration, Plus is the name of the class, α : Type is the only argument, and plus : α → α → α is the only method:

class Plus (α : Type) where
  plus : α → α → α

> MISTAKE GOES HERE

Activity

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

    No labels
    No labels

    Type

    No type

    Projects

    No projects

      Milestone

      No milestone

      Relationships

      None yet

      Development

      No branches or pull requests

      Issue actions