All pull requests

Pull requests

• Two recursive types that spell the same tree are the same type

  #2777·7h3kk1d opened Oct 30, 2026Contributor·5/6·

  ·

• MakeTerm: parse projections at every sort; print module-pattern holes

  #2770·cyrus- opened Oct 29, 2026Member·

  ·
  1

• Route definition-form checks through one exhaustive DefForm helper

  #2769·cyrus- opened Oct 29, 2026Member·

  ·
  1

• Look through Parens and Projector wherever statics, elaboration and proofs inspect a head

  #2768·cyrus- opened Oct 29, 2026Member·

  ·
  6

• Fix bugs hidden by catch-alls in the agent, editors, stepper and TyDi; make guards exhaustive

  #2767·cyrus- opened Oct 29, 2026Member·

  ·
  1

• Projectors: see through Parens and Projector wrappers consistently

  #2766·cyrus- opened Oct 29, 2026Member·

  ·
  1

• Fix derivation subst under case binders, rec glb, and ModLet pattern equality

  #2765·cyrus- opened Oct 29, 2026Member·

  ·
  1

• Keep hover and automatic settings updates out of undo history

  #2764·cyrus- opened Oct 29, 2026Member·

  ·
  1

• Draw the editor context menu in the top layer

  #2763·cyrus- opened Oct 29, 2026Member·

  ·
  1

  1

• Keep probe pins through streamed re-runs; stream at most every 500 ms

  #2762·Negabinary opened Oct 29, 2026Contributor·

  ·
  1

• Advisory per-PR performance report

  #2756·cyrus- opened Oct 29, 2026Member·

  ·
  2

• Tests: a module's sum types at the edges (signatures, shadowing, nesting)

  #2749·matthewhammer opened Oct 29, 2026Member·

  ·
  1

• Documentation slide: Recursive Types

  #2739·7h3kk1d opened Oct 26, 2026Contributor·6/6·

  ·

• A type defined as itself is warned where it is written

  #2738·7h3kk1d opened Oct 26, 2026Contributor·4/6·

  ·
  1

• Typ.meet compares recursive and polymorphic types under the binder they share

  #2737·7h3kk1d opened Oct 26, 2026Contributor·1/6·

  ·
  1

• Check against a recursive type through its unrolling

  #2736·7h3kk1d opened Oct 26, 2026Contributor·3/6·

  ·
  1

• Typ.unroll unrolls to the first non-Rec head, and is None on a non-contractive type

  #2734·7h3kk1d opened Oct 26, 2026Contributor·2/6·

  ·
  1

  7

• Make matched-type handling explicit in statics

  #2733·Negabinary opened Oct 26, 2026Contributor·3/3·

  ·
  1

  1

• A type binder that reuses a name in scope is renamed with its scope

  #2732·7h3kk1d opened Oct 26, 2026Contributor·

  ·
  7

• Go to next usage (Shift+F12)

  #2731·john-yang-11 opened Oct 25, 2026·

  ·
  1

  8

• A module's sum types are usable after it: their names and constructors

  #2729·matthewhammer opened Oct 23, 2026Member·

  ·
  2

• Use Core's Char and String where Stdlib's were still named

  #2727·7h3kk1d opened Oct 23, 2026Contributor·22/22·

  ·
  2

• Move Stdlib.Hashtbl users onto Core's Hashtbl and Hash_set

  #2726·7h3kk1d opened Oct 23, 2026Contributor·21/22·

  ·
  2

• Replace the remaining local Stdlib maps and sets with Core's

  #2725·7h3kk1d opened Oct 23, 2026Contributor·20/22·

  ·
  1

• Move Id.Map and Id.Set onto Core's tree maps and sets

  #2724·7h3kk1d opened Oct 23, 2026Contributor·19/22·

  ·
  1