All pull requests

Pull requests

• fix: keep declarations that cannot be auto-quoted in the unquoted local context

  #177·josaum opened Nov 8, 2026·

  ·
  1

  1

• fix: support level antiquotations in explicit universe annotations x.{$u}

  #176·josaum opened Nov 7, 2026·

  ·
  1

• fix: determine the ~q discriminant's universe level from its unquoted type

  #175·josaum opened Nov 5, 2026·

  ·
  1

• fix: record level-variable TermInfos at antiquotations, not the quotation body

  #174·josaum opened Nov 3, 2026·

  ·
  1

• fix: support let mut in capture-free if let ~q branches

  #173·josaum opened Nov 2, 2026·

  ·

• fix: don't leak metavariables from postponed elaboration in ~q match bodies

  #172·josaum opened Nov 1, 2026·

  ·
  1

• fix: don't treat let-bound aliases as canonical instances in assertInstancesCommute

  #171·josaum opened Oct 31, 2026·

  ·
  1

• docs: fix the two broken README examples (betterApp, List ((u : Level) × ...))

  #169·josaum opened Oct 26, 2026·

  ·
  1

• fix: preserve auxDeclToFullName when unquoting the local context

  #168·josaum opened Oct 20, 2026·

  ·
  1

• fix: treat none as a refutable qq match pattern

  #159·chessing234 opened Aug 31, 2026·2 tasks·

  ·

• fix: don't fail delaboration with errors

  #150·Rob23oba opened Jul 4, 2026Contributor·

  ·
  2

• feat: wrapper components with =Q(L) hypotheses

  #146·thorimur opened Jun 1, 2026Collaborator·

  ·

• chore: adaptations for leanprover/lean4#13305

  #145·sgraf812 opened May 30, 2026Contributor·

  ·

• fix: Application type mismatch (was throwing after https://github.com/leanprover/lean4/pull/13030)

  #141·srghma opened Apr 21, 2026·

  ·
  2

• refactor: replace assert!-based hacks with doElem elaborator for ~q()

  #140·sgraf812 opened Apr 17, 2026Contributor·

  ·
  2

• feat: implement ~ql() matching

  #102·eric-wieser opened Sep 23, 2025Member·

  ·

• fix: make goto definition work on quoted variables

  #90·eric-wieser opened Jun 30, 2025Member·

  ·
  7

• feat: return QuotedDefEq from Meta wrappers

  #68·eric-wieser opened Jan 14, 2025Member·

  ·

• feat: allow interpolation of fvars, with a warning

  #64·eric-wieser opened Nov 2, 2024Member·

  ·

• Fix #16

  #50·eric-wieser opened Aug 18, 2024Member·

  ·

• Attempt to fix #21

  #27·eric-wieser opened Nov 15, 2023Member·

  ·

• Ensure shadowed variables are inaccessible in quotations

  #11·alexkeizer opened Apr 17, 2023·

  ·
  2