Skip to content

Redefining Data.Nat.DivMod.DivMod #2221

@jamesmckinna

Description

@jamesmckinna

[tagged as v2.0, because this is a last opportunity to break this now before v3.0]

Why does the record definition DivMod not take an additional irrelevant instance argument .{{_ : NonZero divisor}} as part its definition?

Two potential knock-on consequences of the change:

  • the entire section could then be defined in a single module (modulo fixing up the infix declarations)? (But such a refactoring could be done downstream in v2.(n+1))
  • use of the specification and its implementation(s) then enforces an additional compile-time check on client modules (maybe there are pros and cons to this?)

Re: the last point. Only knock-on consequence appears to be the need to (re-)instate {{_ : NonZero divisor}} in the type of _divMod_ in place of the current {{ NonZero divisor }} in Data.Nat.DivMod.WithK...

Metadata

Metadata

Assignees

No one assigned

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions