All pull requests

Pull requests

• Adaptations for Lean 4.35

  #47·Kha opened Sep 9, 2026·

  ·

• Iota Reduction

  #43·barabbs opened Aug 8, 2026·

  ·
  10

• prove shape compatibility is preserved by lifting

  #42·arthurpaulino opened Aug 4, 2026·

  ·

• prove bottom shape function application

  #41·arthurpaulino opened Aug 4, 2026·

  ·

• prove finite order reflexivity

  #40·arthurpaulino opened Aug 4, 2026·

  ·

• prove weak-head reduction weakening

  #39·arthurpaulino opened Aug 4, 2026·

  ·

• prove substitution lookup preserves definitional equality

  #38·arthurpaulino opened Aug 4, 2026·

  ·

• fix: prove the TreeMap.all equation

  #36·arthurpaulino opened Aug 4, 2026·

  ·

• feat: prove Level cached-flag correctness

  #27·kim-em opened Aug 2, 2026Contributor·

  ·
  1

  2

• Fix constDF case in Stratified induction

  #15·heathsanchez opened Jul 5, 2026·

  ·

• Fix constDF case in StratifiedUntyped induction

  #14·heathsanchez opened Jul 5, 2026·

  ·

• feat: use module system -> add module keyword to the top

  #13·srghma opened May 22, 2026Contributor·

  ·

• feat: parse and check a lean4export file

  #10·nomeata opened Jan 10, 2026Contributor·

  ·

• opt: fvar reuse optimization

  #5·rish987 opened Nov 5, 2024Contributor·

  ·

• Feat : Github Actions for keeping up with toolchain

  #4·Shreyas4991 opened Oct 10, 2024·

  ·

• docs: add documentation for inductive types

  #3·rish987 opened Jul 14, 2024Contributor·

  ·

• docs: document defeq and type inference related functions

  #2·rish987 opened May 17, 2024Contributor·

  ·
  6