All pull requests

Pull requests

• Projector stack element for reduction

  #4638·amosr-msft opened Oct 3, 2026Contributor·

  ·
  2

• Improve and use core typechecker in place of tcterm in phase 2

  #4605·nikswamy opened Sep 26, 2026Contributor·

  ·
  2

• SMT: state ground typing facts for refined pure applications (#4591)

  #4602·gebner opened Sep 25, 2026Contributor·

  ·
  1

  2

• Restate quantifier-free argument refinements at lemma calls (fixes #4591)

  #4597·gebner opened Sep 24, 2026Contributor·

  ·
  1

  2

• Batch tactic proof obligations that share a context into one SMT query

  #4557·gebner opened Sep 22, 2026Contributor·

  ·
  3

• Fix record projection normalizer performance regression

  #4538·gebner opened Sep 10, 2026Contributor·

  ·
  1

  1

• SMT encoding: eliminate unit-refinement binders in favor of implications

  #4524·gebner opened Sep 3, 2026Contributor·

  ·
  4

• Eta-expand product-typed holes in Pulse

  #4497·hei411 opened Aug 27, 2026Collaborator·

  ·
  1

• Pulse: only drop leaked branch refinements, fixing #4488 rlimit regression

  #4496·gebner opened Aug 27, 2026Contributor·

  ·
  1

• tools/depgraph

  #4464·nikswamy opened Aug 22, 2026Contributor·

  ·
  1

• Pulse: purify stateful-read sugar in call arguments (fixes #4423)

  #4424·hei411 opened Aug 12, 2026Collaborator·

  ·
  1

  3

• Change book's LaTeX engine to XeLaTex

  #4413·smheidrich opened Aug 10, 2026Contributor·

  ·

• Mention Unicode forms of syntax elements in book

  #4412·smheidrich opened Aug 10, 2026Contributor·

  ·
  1

  1

• Differential tests and patches to NBE to match its behavior with the normalizer

  #4398·nikswamy opened Aug 7, 2026Contributor·

  ·

• Pulse: introduce let rewrite

  #4342·mtzguido opened Jun 29, 2026Member·

  ·
  1

• Sketch Pulse short-circuiting for stateful boolean operands

  #4336·eluvane opened Jun 26, 2026Contributor·

  ·
  1

• Pulse: let-bind applications on return

  #4315·mtzguido opened Jun 11, 2026Member·

  ·
  1

• Remove unnecessary coercions between bool/prop/Type

  #4279·gebner opened May 26, 2026Contributor·

  ·

• Do not force type constructors to be injective

  #4259·nikswamy opened May 14, 2026Contributor·

  ·
  1

• 4244

  #4246·mtzguido opened May 5, 2026Member·

  ·
  2

• Bump to Z3 4.16.0

  #4218·mtzguido opened Apr 25, 2026Member·

  ·
  2

• Skip redundant phase1 TC passes when no uvars are left

  #4183·nikswamy opened Apr 9, 2026Contributor·

  ·
  1

• Fix --use_nbe_for_extraction option

  #4179·mtzguido opened Apr 8, 2026Member·

  ·

• Add shift_arithmetic_left for signed integers

  #4112·remix7531 opened Mar 2, 2026Contributor·

  ·
  1

• Fix cross-platform build: replace symlinks with copy_files

  #4085·elefthei opened Jan 16, 2026Contributor·

  ·
  10