Skip to content

Document what should live here, vs in mathlib #1576

@414owen

Description

@414owen

Coming from Haskell, I would have expected Bifunctor to be here.
Is there a set of rules, for deciding where things should live?
I'm trying to avoid importing mathlib, at the moment, because I'm working on programming, rather than theorem proving.

Metadata

Metadata

Assignees

No one assigned

    Labels

    documentationImprovements or additions to documentationquestionFurther information is requested

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions