Skip to content

support for scoped and local default instances #6604

@leodemoura

Description

@leodemoura

The attribute default_instance currently does not support local and scoped modifiers.
Motivation:

/-- info: 1 + 2 : Nat -/
#guard_msgs in #check 1 + 2

@[local default_instance 101]  -- Error: `default_instance` must be global
instance instOfNatInt (n : Nat) : OfNat Int n where
  ofNat := n

/-- info: 1 + 2 : Int -/
#guard_msgs in #check 1 + 2

Metadata

Metadata

Assignees

No one assigned

    Labels

    P-mediumWe may work on this issue if we find the timebugSomething isn't working

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions