Commits

Branch selector

 master

User selector

nomeata

Datepicker

All time

Commit History

Commits on Jan 2, 2025

• feat: partial_fixpoint: monotonicity tactic (#6506)

  Show description for e9f0691
  nomeata

  authored
  e9f0691

  Copy full SHA for e9f0691

• feat: partial_fixpoint: theory (#6477)

  Show description for 7d0c0d4
  nomeata

  authored
  7d0c0d4

  Copy full SHA for 7d0c0d4

Commits on Dec 10, 2024

• refactor: ArgsPacker.unpack to return Option (#6359)

  Show description for d27c5af
  nomeata

  authored
  d27c5af

  Copy full SHA for d27c5af

• refactor: elabWFRel to take names, not PreDefinition (#6358)

  Show description for 9386511
  nomeata

  authored
  9386511

  Copy full SHA for 9386511

• refactor: WF.EqnInfo.hasInduct (#6357)

  Show description for a9b6a9a
  nomeata

  authored
  a9b6a9a

  Copy full SHA for a9b6a9a

• refactor: make mkInhabitantFor error message configurable (#6356)

  Show description for d5b565e
  nomeata

  authored
  d5b565e

  Copy full SHA for d5b565e

Commits on Dec 7, 2024

• feat: FunInd: omit unused parameters (#6330)

  Show description for 6447fda
  nomeata

  committed
  6447fda

  Copy full SHA for 6447fda

• chore: update stage0

  nomeata

  committed
  279f36b

  Copy full SHA for 279f36b

• feat: FunInd: omit unused parameters (#6330)

  Show description for d2853ec
  nomeata

  committed
  d2853ec

  Copy full SHA for d2853ec

Commits on Nov 23, 2024

• doc: refine kernel code comments (#6150)

  Show description for bf13b24
  nomeata

  authored
  bf13b24

  Copy full SHA for bf13b24

Commits on Nov 18, 2024

• fix: handle reordered indices in structural recursion (#6116)

  Show description for 799b2b6
  nomeata

  authored
  799b2b6

  Copy full SHA for 799b2b6

Commits on Nov 15, 2024

• refactor: use mkFreshUserName in ArgsPacker (#6093)

  Show description for 93b4ec0
  nomeata

  authored
  93b4ec0

  Copy full SHA for 93b4ec0

Commits on Nov 14, 2024

• perf: use RArray in simp_arith meta code (#6068 part 2)

  Show description for 6a5b122
  

  nomeata

  authored and

  Kha

  committed
  6a5b122

  Copy full SHA for 6a5b122

• chore: update stage0

  

  nomeata

  authored and

  Kha

  committed
  bf9ddf2

  Copy full SHA for bf9ddf2

• perf: use RArray in simp_arith meta code (#6068 part 1)

  Show description for 3f47871
  

  nomeata

  authored and

  Kha

  committed
  3f47871

  Copy full SHA for 3f47871

• feat: Lean.RArray (#6070)

  Show description for 85f2596
  nomeata

  authored
  85f2596

  Copy full SHA for 85f2596

Commits on Nov 13, 2024

• perf: optimize Nat.Linear.Poly.norm (#6064)

  Show description for 256b49b
  nomeata

  authored
  256b49b

  Copy full SHA for 256b49b

• perf: optimize Nat.Linear.Expr.toPoly (#6062)

  nomeata

  authored
  970261b

  Copy full SHA for 970261b

• test: synthetic simp_arith benchmark (#6061)

  Show description for 6b811f8
  nomeata

  authored
  6b811f8

  Copy full SHA for 6b811f8

• refactor: omega: avoid MVar machinery (#5991)

  Show description for f18d9e0
  nomeata

  authored
  f18d9e0

  Copy full SHA for f18d9e0

• chore: pr-body: run as part of merge_group, but do not do anything (#6069)

  nomeata

  authored
  fa33423

  Copy full SHA for fa33423

Commits on Nov 11, 2024

• fix: simp only [· ∈ ·] (#6030)

  Show description for 5c611f7
  nomeata

  authored
  5c611f7

  Copy full SHA for 5c611f7

Commits on Nov 7, 2024

• refactor: name the default SizeOf instance (#5981)

  Show description for 70435df
  nomeata

  authored
  70435df

  Copy full SHA for 70435df

Commits on Oct 31, 2024

• fix: FunInd: unfold aux definitions more carefully (#5904)

  Show description for 008537a
  nomeata

  authored
  008537a

  Copy full SHA for 008537a

Commits on Oct 30, 2024

• fix: declareSimpLikeTactic macro to use mkSynthetic (#5838)

  Show description for 0d12618
  nomeata

  authored
  0d12618

  Copy full SHA for 0d12618

Commits on Oct 29, 2024

• feat: attribute [simp ←] (#5870)

  Show description for 6514385
  nomeata

  authored
  6514385

  Copy full SHA for 6514385

Commits on Oct 26, 2024

• fix: deprecations in Init.Data.Array.Basic (#5848)

  nomeata

  authored
  8f0328b

  Copy full SHA for 8f0328b

• refactor: Predefinition.Structural code cleanup (#5850)

  Show description for 38490a4
  nomeata

  authored
  38490a4

  Copy full SHA for 38490a4

Commits on Oct 25, 2024

• test: test case for #5836 (#5843)

  nomeata

  authored
  57a95c8

  Copy full SHA for 57a95c8

Commits on Oct 22, 2024

• doc: refine rwa docstring (#5811)

  Show description for eddbdd7
  nomeata

  authored
  eddbdd7

  Copy full SHA for eddbdd7

• chore: nix-ci.yml: fix test-results.xml path (#5804)

  nomeata

  authored
  bab6aff

  Copy full SHA for bab6aff

• fix: FunInd: withLetDecl and mkLetVar don’t mix (#5803)

  Show description for 5bea46d
  nomeata

  authored
  5bea46d

  Copy full SHA for 5bea46d

Commits on Oct 21, 2024

• fix: RecursorVal.getInduct to return name of major argument’s type (#5679)

  Show description for 76164b2
  nomeata

  authored
  76164b2

  Copy full SHA for 76164b2

Commits on Oct 18, 2024

• fix: structural nested recursion confused when nested type appears first (#5766)

  Show description for 26df545
  nomeata

  authored
  26df545

  Copy full SHA for 26df545

Commits on Oct 17, 2024

• doc: remove docstring from implicitDefEqProofs (#5751)

  Show description for 08d8a08
  nomeata

  authored
  08d8a08

  Copy full SHA for 08d8a08

Pagination

Previous

Next