Commits

Branch selector

 main

User selector

digama0

Datepicker

All time

Commit History

Commits on Feb 6, 2024

• feat: generate minimal structure instances in code action (leanprover-community#577)

  digama0

  authored
  4695a26

Commits on Jan 11, 2024

• feat: false_or_by_contra uses Decidable.byContra if possible (leanprover-community#519)

  Show description for b33ce1b
  

  4 peopleauthored
  b33ce1b

Commits on Jan 4, 2024

• feat: more simp lemmas for bind_eq_some (leanprover-community#487)

  digama0

  authored
  c4e111b

Commits on Jan 1, 2024

• fix: synthesize pending mvars after rcases (leanprover-community#493)

  digama0

  authored
  a035269

• fix: synthesizeSyntheticMVarsNoPostponing in rcases subst

  digama0

  committed
  baaa291

Commits on Dec 4, 2023

• fix: Use MLList.uncons? to avoid stack overflow (leanprover-community#407)

  Show description for 5ab9a47
  

  digama0

  and

  kim-em

  authored
  5ab9a47

Commits on Nov 22, 2023

• feat: array lemmas for Array.forIn

  digama0

  committed
  282e3a1

Commits on Nov 17, 2023

• feat: runLinter calls lake build if needed

  digama0

  committed
  d304964

• chore: use lean_exe srcDir in lakefile

  digama0

  committed
  0da920c

Commits on Nov 15, 2023

• chore: reduce imports in Tactic.Lint.TypeClass

  digama0

  committed
  ebc61da

Commits on Nov 5, 2023

• chore: update nolints

  Show description for 6a5a33b
  digama0

  committed
  6a5a33b

Commits on Nov 3, 2023

• feat: Array.contains_def

  digama0

  committed
  9bfbd2a

Commits on Nov 1, 2023

• chore: add lake-manifest.json to .gitignore

  digama0

  committed
  5719bd8

• chore: remove lake-manifest.json

  Show description for 026b17c
  digama0

  committed
  026b17c

Commits on Oct 22, 2023

• chore: := syntax in package is deprecated

  digama0

  committed
  d83bd03

Commits on Oct 20, 2023

• fix: repeat' should roll back the state (leanprover-community#305)

  Show description for e3f238c
  digama0

  authored
  e3f238c

Commits on Oct 13, 2023

• feat: add Float.{toRatParts, toStringFull} (leanprover-community#282)

  digama0

  authored
  846e9e1

Commits on Oct 10, 2023

• chore: update lean

  digama0

  committed
  68517fc

Commits on Sep 25, 2023

• fix: match indentation

  digama0

  committed
  86b0eca

Commits on Sep 24, 2023

• fix: don't count parameters as minor premises

  Show description for 9d01490
  digama0

  committed
  9d01490

Commits on Sep 17, 2023

• fix: add lakefile.olean to .gitignore

  digama0

  committed
  7ed3892

• fix: allow guard_hyp h with no type and expr

  digama0

  committed
  cab81d7

Commits on Sep 8, 2023

• fix: support code action for 'cases e with'

  digama0

  committed
  14e723a

• fix: make 'try this' a preferred code action

  digama0

  committed
  75d9264

Commits on Aug 30, 2023

• fix: panic in induction code action

  Show description for dd3a248
  digama0

  committed
  dd3a248

Commits on Aug 28, 2023

• feat: code action for alias + deprecated (leanprover-community#231)

  Show description for 7194b6b
  digama0

  authored
  7194b6b

Commits on Aug 25, 2023

• feat: alias sets the deprecated target (leanprover-community#228)

  Show description for e8f2307
  digama0

  authored
  e8f2307

Commits on Jul 6, 2023

• feat: Data.Fin.Lemmas <- mathlib (leanprover-community#173)

  digama0

  authored
  cd11695

Commits on Jul 3, 2023

• fix: blacklist notation / mixfix in unreachableTactic

  digama0

  committed
  0d260d4

• feat: support set_option in in linters

  digama0

  committed
  58c10a6

Commits on Jul 2, 2023

• chore: update lean 07-01

  digama0

  committed
  dff883c

Commits on Jun 29, 2023

• chore: update lean 06-28

  digama0

  committed
  1542e1c

• chore: remove workaround

  digama0

  committed
  cfb9fee

Commits on Jun 28, 2023

• fix: doc

  digama0

  committed
  1c4ac57

• fix: use no_implicit_lambda% in show_term

  Show description for 8f1b5aa
  digama0

  committed
  8f1b5aa

Pagination

PreviousNext