Commits

Breadcrumbs

History for

onmaster

User selector

All users

Datepicker

All time

Commit History

Commits on Oct 12, 2022

• feat: add implementation-detail hypotheses

  gebner

  committed
  ba57ad3

  Copy full SHA for ba57ad3

Commits on Aug 15, 2022

• chore: improve check traces

  

  gebner

  authored and

  leodemoura

  committed
  d5eb9f3

  Copy full SHA for d5eb9f3

Commits on Jul 28, 2022

• doc: add some doc strings

  leodemoura

  committed
  388163e

  Copy full SHA for 388163e

Commits on Jul 26, 2022

• chore: cleanup

  leodemoura

  committed
  3896244

  Copy full SHA for 3896244

• refactor: improve FVarId method discoverability

  Show description for 90fb110
  leodemoura

  committed
  90fb110

  Copy full SHA for 90fb110

Commits on Jul 22, 2022

• chore: convert doc/mod comments from /- to /--//-! (leanprover#1354)

  digama0

  authored
  f6211b1

  Copy full SHA for f6211b1

Commits on Jul 11, 2022

• refactor: use computed fields for Expr

  

  gebner

  authored and

  leodemoura

  committed
  a8cab84

  Copy full SHA for a8cab84

Commits on Jul 10, 2022

• perf: add cache for check (e : Expr) : MetaM Unit

  Show description for 23bae26
  leodemoura

  committed
  23bae26

  Copy full SHA for 23bae26

Commits on Jul 2, 2022

• chore: use a[i]! for array accesses that may panic

  leodemoura

  committed
  2ebcf29

  Copy full SHA for 2ebcf29

Commits on Jun 8, 2022

• chore: unused variables

  leodemoura

  committed
  041827b

  Copy full SHA for 041827b

Commits on Jun 7, 2022

• refactor: unname some unused variables

  

  Kha

  authored and

  leodemoura

  committed
  ae7b895

  Copy full SHA for ae7b895

Commits on Feb 4, 2022

• chore: fix codebase after removing auto pure

  leodemoura

  committed
  12e2a79

  Copy full SHA for 12e2a79

Commits on Dec 6, 2021

• refactor: ExprDefEq.lean and LevelDefEq.lean are now implementation only files

  Show description for 7b6732a
  leodemoura

  committed
  7b6732a

  Copy full SHA for 7b6732a

Commits on Nov 9, 2021

• fix: bug at addPPExplicitToExposeDiff

  leodemoura

  committed
  84d4d77

  Copy full SHA for 84d4d77

Commits on Mar 11, 2021

• chore: throwError! => throwError, throwErrorAt! => throwErrorAt

  Show description for be841a7
  leodemoura

  committed
  be841a7

  Copy full SHA for be841a7

• chore: trace[...]! ==> trace[...]

  Show description for 68143ca
  leodemoura

  committed
  68143ca

  Copy full SHA for 68143ca

Commits on Mar 8, 2021

• feat: include type of type in "mismatch errors"

  Show description for 5d3f060
  leodemoura

  committed
  5d3f060

  Copy full SHA for 5d3f060

Commits on Feb 11, 2021

• chore: naming convention

  leodemoura

  committed
  5e0b6a4

  Copy full SHA for 5e0b6a4

Commits on Jan 27, 2021

• chore: cleanup

  leodemoura

  committed
  75466a7

  Copy full SHA for 75466a7

Commits on Dec 17, 2020

• feat: improve type mismatch error messages

  Show description for c7ae835
  leodemoura

  committed
  c7ae835

  Copy full SHA for c7ae835

Commits on Dec 9, 2020

• feat: improve application type mismatch error message

  Show description for 7a4b544
  leodemoura

  committed
  7a4b544

  Copy full SHA for 7a4b544

Commits on Dec 8, 2020

• chore: add explicit discard

  leodemoura

  committed
  ae5aa51

  Copy full SHA for ae5aa51

Commits on Nov 25, 2020

• chore: cleanup Check.lean

  leodemoura

  committed
  36eb03c

  Copy full SHA for 36eb03c

Commits on Nov 14, 2020

• refactor: move Ref to Prelude and rename it to MonadRef

  Show description for 396e767
  leodemoura

  committed
  396e767

  Copy full SHA for 396e767

Commits on Oct 26, 2020

• chore: cleanup

  leodemoura

  committed
  5481999

  Copy full SHA for 5481999

Commits on Oct 25, 2020

• chore: remove #lang lean4 header

  leodemoura

  committed
  13c2a8f

  Copy full SHA for 13c2a8f

Commits on Oct 19, 2020

• chore: use builtin_initialize instead of initialize at src/Lean

  leodemoura

  committed
  1495f40

  Copy full SHA for 1495f40

• chore: move to new frontend

  leodemoura

  committed
  9abe45a

  Copy full SHA for 9abe45a

Commits on Sep 22, 2020

• fix: throwAppTypeMismatch should be polymorphic

  Show description for bbc1f4d
  leodemoura

  committed
  bbc1f4d

  Copy full SHA for bbc1f4d

Commits on Sep 12, 2020

• refactor: add DefEqM

  Show description for e181c1a
  leodemoura

  committed
  e181c1a

  Copy full SHA for e181c1a

Commits on Sep 9, 2020

• fix: error message

  leodemoura

  committed
  02fc447

  Copy full SHA for 02fc447

Commits on Sep 4, 2020

• chore: change meaning of lambdaTelescope

  Show description for 12f69a7
  leodemoura

  committed
  12f69a7

  Copy full SHA for 12f69a7

Commits on Sep 3, 2020

• feat: preserve nonDep flag at LocalDecl.ldecl

  leodemoura

  committed
  238c38f

  Copy full SHA for 238c38f

Commits on Aug 28, 2020

• chore: cleanup

  leodemoura

  committed
  4bc1be1

  Copy full SHA for 4bc1be1

Commits on Aug 24, 2020

• refactor: add MonadMetaM class

  leodemoura

  committed
  ac565de

  Copy full SHA for ac565de

Pagination

Previous

Next