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

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