All pull requests

Pull requests

• Keep elaboration decisions from the final name-resolution pass

  #6303·runarorama opened Sep 30, 2026Contributor·

  ·

• Accept dictionary elaboration only after core verification

  #6302·runarorama opened Sep 30, 2026Contributor·

  ·

• Resolve source givens from their completed binding schemes

  #6301·runarorama opened Sep 30, 2026Contributor·

  ·

• Preserve source given scope across dependency grouping

  #6300·runarorama opened Sep 30, 2026Contributor·

  ·

• Record completed given schemes for deferred resolution

  #6299·runarorama opened Sep 30, 2026Contributor·

  ·

• Build complete dictionary plans independently of note order

  #6298·runarorama opened Sep 30, 2026Contributor·

  ·

• Introduce dictionary parameters while checking qualified definitions

  #6297·runarorama opened Sep 30, 2026Contributor·

  ·

• Order generated dictionary parameters within source scopes

  #6296·runarorama opened Sep 30, 2026Contributor·

  ·

• Capture lexical givens by their active binder identities

  #6295·runarorama opened Sep 30, 2026Contributor·

  ·

• Record dictionary goals at precise checker application sites

  #6294·runarorama opened Sep 30, 2026Contributor·

  ·

• Require determined goal types before dictionary search

  #6293·runarorama opened Sep 30, 2026Contributor·

  ·

• Insert dictionaries at identified expression sites

  #6292·runarorama opened Sep 30, 2026Contributor·

  ·

• Identify lexical dictionary bindings without changing source diagnostics

  #6291·runarorama opened Sep 30, 2026Contributor·

  ·

• Track expression identity separately from source location

  #6290·runarorama opened Sep 30, 2026Contributor·

  ·

• Check implicit arrows without erasing dictionary requirements

  #6289·runarorama opened Sep 30, 2026Contributor·

  ·

• Keep effect rows outside implicit constraint contexts

  #6288·runarorama opened Sep 30, 2026Contributor·

  ·

• Track given membership in namespace metadata

  #6287·runarorama opened Sep 30, 2026Contributor·

  ·

• Verify explicit dictionary bodies before accepting elaboration

  #6286·runarorama opened Sep 30, 2026Contributor·

  ·

• Decompose qualified signatures into dictionary candidates

  #6285·runarorama opened Sep 30, 2026Contributor·

  ·

• Handle implicit parameters in function-type utilities

  #6276·runarorama opened Sep 30, 2026Contributor·

  ·

• Represent and store implicit function arrows

  #6275·runarorama opened Sep 30, 2026Contributor·

  ·

• Bound the size of generated implicit goals

  #6274·runarorama opened Sep 30, 2026Contributor·

  ·

• Prefer strictly more specific dictionary conclusions

  #6273·runarorama opened Sep 30, 2026Contributor·

  ·

• Resolve dictionary premises with bounded, context-sensitive search

  #6272·runarorama opened Sep 30, 2026Contributor·

  ·

• Match polymorphic dictionaries without solving goal variables

  #6271·runarorama opened Sep 30, 2026Contributor·

  ·