Commits

Branch selector

 master

User selector

kmill

Datepicker

All time

Commit History

Commits on Mar 4, 2025

• chore: re-enable synthesis checkpoint for structure parent elaboration (#7314)

  Show description for 48491e5
  kmill

  authored
  48491e5

  Copy full SHA for 48491e5

Commits on Mar 3, 2025

• chore: reimplement mk_projections in Lean (#7295)

  Show description for e3c6909
  kmill

  authored
  e3c6909

  Copy full SHA for e3c6909

Commits on Feb 23, 2025

• chore: post-#7100 cleanup (#7196)

  Show description for b863ca9
  kmill

  authored
  b863ca9

  Copy full SHA for b863ca9

Commits on Feb 18, 2025

• chore: review uses of generalize (#7126)

  Show description for 2d4c001
  kmill

  authored
  2d4c001

  Copy full SHA for 2d4c001

• feat: make structure parent projections nameable (#7100)

  Show description for 7557542
  kmill

  authored
  7557542

  Copy full SHA for 7557542

• chore: cleanup after stage0 update for #7103 (#7125)

  Show description for 219f36f
  kmill

  authored
  219f36f

  Copy full SHA for 219f36f

• feat: add generalization hypotheses to induction tactic (#7103)

  Show description for 6a59926
  kmill

  authored
  6a59926

  Copy full SHA for 6a59926

Commits on Feb 14, 2025

• feat: make binders in #check be hoverable (#7074)

  Show description for 1babe9f
  kmill

  authored
  1babe9f

  Copy full SHA for 1babe9f

Commits on Feb 8, 2025

• doc: mention Props are equal to True or False (#6998)

  Show description for dd293d1
  kmill

  authored
  dd293d1

  Copy full SHA for dd293d1

Commits on Feb 4, 2025

• fix: make rewrite/rw tactic abort on elaboration errors (#6891)

  Show description for 23bd9df
  kmill

  authored
  23bd9df

  Copy full SHA for 23bd9df

Commits on Feb 2, 2025

• feat: make all app unexpanders respond to pp.tagAppFns (#6730)

  Show description for 1f6abca
  kmill

  authored
  1f6abca

  Copy full SHA for 1f6abca

• feat: make coeFun delaborator respect pp.tagAppFns (#6729)

  Show description for 89d897a
  kmill

  authored
  89d897a

  Copy full SHA for 89d897a

• feat: modify delaborator to tag generalized field notation (#6703)

  Show description for 3fb264b
  kmill

  authored
  3fb264b

  Copy full SHA for 3fb264b

Commits on Jan 8, 2025

• feat: let induction take zero alteratives (#6486)

  Show description for 18b183f
  kmill

  authored
  18b183f

  Copy full SHA for 18b183f

Commits on Dec 31, 2024

• fix: make sure parent structure projections have 'go to definition' information (#6487)

  Show description for 6d44715
  kmill

  authored
  6d44715

  Copy full SHA for 6d44715

• chore: add missing diff-exposing in type/value mismatch errors (#6484)

  Show description for 640b356
  kmill

  authored
  640b356

  Copy full SHA for 640b356

• feat: upstream ToExpr deriving handler from Mathlib (#6473)

  Show description for 8f5ce3a
  

  kmill

  and

  alexkeizer

  authored
  8f5ce3a

  Copy full SHA for 8f5ce3a

Commits on Dec 21, 2024

• feat: explanations for cases applied to non-inductive types (#6378)

  Show description for 7194263
  kmill

  authored
  7194263

  Copy full SHA for 7194263

Commits on Dec 19, 2024

• fix: process delayed assignment metavariables correctly in Lean.Meta.Closure (#6414)

  Show description for 12cadda
  kmill

  authored
  12cadda

  Copy full SHA for 12cadda

Commits on Dec 17, 2024

• chore: in #print for structures, mention 'field notation' (#6406)

  Show description for 64d3e9a
  kmill

  authored
  64d3e9a

  Copy full SHA for 64d3e9a

Commits on Dec 11, 2024

• feat: labeled and unique sorries (#5757)

  Show description for 58f8e21
  kmill

  authored
  58f8e21

  Copy full SHA for 58f8e21

Commits on Dec 10, 2024

• fix: when pretty printing constant names, do not use aliases from "non-API exports" (#5689)

  Show description for cd909b0
  kmill

  authored
  cd909b0

  Copy full SHA for cd909b0

Commits on Dec 9, 2024

• chore: release notes for 4.14.0 (#6339)

  kmill

  authored
  3f79193

  Copy full SHA for 3f79193

Commits on Dec 8, 2024

• feat: _ separators in numeric literals (#6204)

  Show description for 63791f0
  kmill

  authored
  63791f0

  Copy full SHA for 63791f0

Commits on Dec 1, 2024

• feat: make "foo has been deprecated" warning be hoverable (#6273)

  Show description for 0a2a8e8
  kmill

  authored
  0a2a8e8

  Copy full SHA for 0a2a8e8

• fix: have Lean.Meta.isConstructorApp'? be aware of n + k Nat offsets (#6270)

  Show description for 23236ef
  kmill

  authored
  23236ef

  Copy full SHA for 23236ef

• chore: post-stage0 cleanup for #6165 (#6268)

  Show description for 7b8504c
  kmill

  authored
  7b8504c

  Copy full SHA for 7b8504c

Commits on Nov 30, 2024

• feat: parity between structure instance notation and where notation (#6165)

  Show description for a1c3a36
  kmill

  authored
  a1c3a36

  Copy full SHA for a1c3a36

• feat: add structInstFieldDecl syntax category (#6265)

  Show description for f3f0045
  kmill

  authored
  f3f0045

  Copy full SHA for f3f0045

Commits on Nov 27, 2024

• feat: expose diff at "synthesized type class instance is not definitionally equal" error (#6213)

  Show description for ce69243
  kmill

  authored
  ce69243

  Copy full SHA for ce69243

Commits on Nov 25, 2024

• feat: make dot notation be affected by export/open (#6189)

  Show description for 606aedd
  kmill

  authored
  606aedd

  Copy full SHA for 606aedd

• feat: add a coercion from List Nat to Lean.Meta.Occurrences (#6206)

  Show description for 0eca3bd
  kmill

  authored
  0eca3bd

  Copy full SHA for 0eca3bd

Commits on Nov 24, 2024

• fix: structures with copied parents can now use other parents as instances (#6175)

  Show description for 2f5c7d0
  kmill

  authored
  2f5c7d0

  Copy full SHA for 2f5c7d0

Commits on Nov 23, 2024

• fix: make sure #check id heeds pp.raw (#6181)

  Show description for ba3f2b3
  kmill

  authored
  ba3f2b3

  Copy full SHA for ba3f2b3

Commits on Nov 22, 2024

• feat: have "motive is not type correct" come with an explanation (#6168)

  Show description for b6a0d63
  kmill

  authored
  b6a0d63

  Copy full SHA for b6a0d63

Pagination

Previous

Next