Commits

Breadcrumbs

History for

onmaster

User selector

All users

Datepicker

All time

Commit History

Commits on Dec 23, 2023

• fix: lsp

  

  tonyxty

  authored and

  alissa-tung

  committed
  e16e139

  Copy full SHA for e16e139

Commits on Dec 22, 2023

• chore: remove workaround in widgets (leanprover#3105)

  Show description for 7c38649
  Vtec234

  authored
  7c38649

  Copy full SHA for 7c38649

Commits on Dec 21, 2023

• fix: hover info for cases h : ... (leanprover#3084)

  Show description for d1a15de
  digama0

  authored
  d1a15de

  Copy full SHA for d1a15de

• chore: default compiler.enableNew to false until development restarts (leanprover#3034)

  Kha

  authored
  bddb215

  Copy full SHA for bddb215

• feat: bundle of widget improvements (leanprover#2964)

  Show description for 8d04ac1
  Vtec234

  authored
  8d04ac1

  Copy full SHA for 8d04ac1

Commits on Dec 20, 2023

• feat: Rust-style raw string literals (leanprover#2929)

  Show description for ae6fe09
  kmill

  authored
  ae6fe09

  Copy full SHA for ae6fe09

• feat: snippet extension (leanprover#3054)

  Show description for 2644b23
  

  Vtec234

  and

  david-christiansen

  authored
  2644b23

  Copy full SHA for 2644b23

Commits on Dec 18, 2023

• feat: add quot_precheck for expression tree elaborators (binop%, etc.) (leanprover#3078)

  Show description for 67bfa19
  kmill

  authored
  67bfa19

  Copy full SHA for 67bfa19

• perf: improve avoidance of repeated Expr visits in unused variables linter (leanprover#3076)

  Show description for 3335b2a
  Kha

  authored
  3335b2a

  Copy full SHA for 3335b2a

• refactor: move unpackArg etc. to WF.PackDomain/WF.PackMutual (leanprover#3077)

  Show description for 7acbee8
  nomeata

  authored
  7acbee8

  Copy full SHA for 7acbee8

• refactor: generalize some simp methods (leanprover#3088)

  leodemoura

  authored
  4dd5969

  Copy full SHA for 4dd5969

• feat: encode let_fun using a letFun function (leanprover#2973)

  Show description for a2226a4
  

  kmill

  and

  Kha

  authored
  a2226a4

  Copy full SHA for a2226a4

Commits on Dec 17, 2023

• doc: fix typos/indentation (leanprover#3085)

  marcusrossel

  authored
  89d7eb8

  Copy full SHA for 89d7eb8

Commits on Dec 16, 2023

• fix: don't panic in leanPosToLspPos (leanprover#3071)

  Show description for 4497aba
  kim-em

  authored
  4497aba

  Copy full SHA for 4497aba

Commits on Dec 14, 2023

• doc: mention x:h@e variant in docstring of x@e (leanprover#3073)

  Show description for 430f4d2
  eric-wieser

  authored
  430f4d2

  Copy full SHA for 430f4d2

Commits on Dec 12, 2023

• feat: test_extern command (leanprover#2970)

  Show description for d4dca3b
  kim-em

  authored
  d4dca3b

  Copy full SHA for d4dca3b

• fix: move Lean.List.toSMap to List.toSMap (leanprover#3035)

  Show description for b120080
  digama0

  authored
  b120080

  Copy full SHA for b120080

• chore: withLocation * should not fail if it closes the main goal (leanprover#2917)

  Show description for 4b8c342
  kim-em

  authored
  4b8c342

  Copy full SHA for 4b8c342

• fix: omit fvars from simp_all? theorem list (leanprover#2969)

  Show description for e2f9571
  JLimperg

  authored
  e2f9571

  Copy full SHA for e2f9571

Commits on Dec 11, 2023

• chore: fix superfluous lemmas in simp.trace (leanprover#2923)

  Show description for 20dd63a
  kim-em

  authored
  20dd63a

  Copy full SHA for 20dd63a

• feat: drop support for termination_by' (leanprover#3033)

  Show description for 5cd90f5
  nomeata

  authored
  5cd90f5

  Copy full SHA for 5cd90f5

Commits on Dec 7, 2023

• fix: GuessLex: deduplicate recursive calls (leanprover#3004)

  Show description for f2a92f3
  nomeata

  authored
  f2a92f3

  Copy full SHA for f2a92f3

• feat: string gaps for continuing string literals across multiple lines (leanprover#2821)

  Show description for bcbcf50
  kmill

  authored
  bcbcf50

  Copy full SHA for bcbcf50

• fix: WF.Fix: deduplicate subsumed goals before running tactic (leanprover#3024)

  Show description for ec8811a
  nomeata

  authored
  ec8811a

  Copy full SHA for ec8811a

Commits on Dec 6, 2023

• doc: fix MetavarContext markdown (leanprover#3026)

  Show description for 5d35e94
  nomeata

  authored
  5d35e94

  Copy full SHA for 5d35e94

Commits on Dec 5, 2023

• feat: detail error message about invalid mutual blocks (leanprover#2949)

  Show description for d4f10bc
  odanoburu

  authored
  d4f10bc

  Copy full SHA for d4f10bc

• feat: GuessLex: print inferred termination argument (leanprover#3012)

  Show description for d6c81f8
  nomeata

  authored
  d6c81f8

  Copy full SHA for d6c81f8

• feat: GuessLex: if no measure is found, explain why (leanprover#2960)

  Show description for 17825bf
  nomeata

  authored
  17825bf

  Copy full SHA for 17825bf

Commits on Dec 4, 2023

• refactor: WF.Fix: gather subgoals (leanprover#3017)

  Show description for 9290b49
  nomeata

  authored
  9290b49

  Copy full SHA for 9290b49

Commits on Dec 2, 2023

• refactor: rewrite TerminationHint elaborators (leanprover#2958)

  Show description for 6d23450
  nomeata

  authored
  6d23450

  Copy full SHA for 6d23450

Commits on Dec 1, 2023

• fix: missing whnf in mkBelowBinder and mkMotiveBinder (leanprover#2991)

  Show description for 66cb44c
  arthur-adjedj

  authored
  66cb44c

  Copy full SHA for 66cb44c

Commits on Nov 30, 2023

• doc: fix typos (leanprover#2996)

  marcusrossel

  authored
  0ad611c

  Copy full SHA for 0ad611c

Commits on Nov 29, 2023

• refactor: CasesOnApp.refineThrough can return a lambda, not an open term (leanprover#2974)

  Show description for 18459cb
  nomeata

  authored
  18459cb

  Copy full SHA for 18459cb

Commits on Nov 27, 2023

• feat: WF.GuessLex: If there is only one plausible measure, use it (leanprover#2954)

  Show description for ffbea84
  nomeata

  authored
  ffbea84

  Copy full SHA for ffbea84

• feat: Guess lexicographic order for well-founded recursion (leanprover#2874)

  Show description for cbba783
  nomeata

  authored
  cbba783

  Copy full SHA for cbba783

Pagination

Previous

Next