All pull requests

Pull requests

• BS-20: the LaTeX backend of the tooling modules as language-1.2 source (first slice of #270)

  #364·humuhumu33 opened Oct 30, 2026Contributor·

  ·

• #276 member 3 (SL-11): canonical JSON writing in the standard library (LexLeanStd.Json) — draft

  #363·humuhumu33 opened Oct 30, 2026Contributor·

  ·

  · LexLean v0.4.2 (Self-hosted compiler)

• Mathlib import: pin, glossary, wrappers, axiom audit, replay cache, demo, design (closes milestone 5)

  #362·humuhumu33 opened Oct 30, 2026Contributor·

  ·

  · Mathlib
  1

• #308 RB-19, BS-09: the lint names of an inner attribute and the segments of a defined path are identifiers

  #361·humuhumu33 opened Oct 30, 2026Contributor·

  ·

  · LexLean v0.4.2 (Self-hosted compiler)

• fix(language-1.2): allow Nat bitwise primitives and shifts

  #332·afflom opened Oct 29, 2026Member·

  ·

• #276 member 2 (SL-10): sorting and order in the standard library (LexLeanStd.Order) — draft

  #328·humuhumu33 opened Oct 27, 2026Contributor·

  ·

• #276 member 1 (SL-09): hexadecimal and decimal in the standard library (LexLeanStd.Numeral) — draft

  #326·humuhumu33 opened Oct 26, 2026Contributor·

  ·

• BS-14: the crate around the bodies of the Rust lowering (RustAssemble)

  #315·afflom opened Oct 25, 2026Member·

  ·

• #91 H7-audit: the crate header, module wrapper, and definitions as RuntimeSyntax nodes; RB-21 and RB-10 tightened; the shared-write plants

  #305·afflom opened Oct 24, 2026Member·

  ·
  5

• #291 PF-25: simplify discharges a conditional lemma from a named hypothesis of the statement

  #303·humuhumu33 opened Oct 23, 2026Contributor·

  ·
  3

• #116: a production root's overflow effect discharged by a kernel-checked bound (PD-09, SP-29; RB-20 red)

  #295·humuhumu33 opened Oct 23, 2026Contributor·

  ·
  4

• SM-37: nested_induction, induction over a nested inductive type through its recursor (#278)

  #292·afflom opened Oct 22, 2026Member·

  ·
  3

• DF-19: structural recursion over the recursive family of a nested inductive type (#278, draft)

  #284·afflom opened Oct 22, 2026Member·

  ·
  3

• [v0.4] #252 four negative fixtures, #251 retitles, claim-audit wording

  #256·afflom opened Oct 21, 2026Member·

  ·
  1

• feat(#30): slice 4 — production of text components, examples/text-models, helper coverage

  #247·afflom opened Oct 20, 2026Member·

  ·
  8

• #115 PR 4/5: SP-24, MD-14, an artifact's decoded value is one literal of the lowered program

  #239·afflom opened Oct 20, 2026Member·

  ·
  3