Commits

Breadcrumbs

History for

onmaster

User selector

All users

Datepicker

All time

Commit History

Commits on Apr 28, 2018

• chore(*): release version 3.4.1

  Kha

  committed
  17fe3de

  Copy full SHA for 17fe3de

Commits on Apr 16, 2018

• chore(*): release version 3.4.0

  leodemoura

  committed
  4be96ea

  Copy full SHA for 4be96ea

Commits on Mar 27, 2018

• refactor(library/init/core,library/init/unit): make unit an abbreviation of punit.{0}

  

  Kha

  authored and

  leodemoura

  committed
  3fefe94

  Copy full SHA for 3fefe94

Commits on Mar 26, 2018

• chore(doc/changes): update changelog

  Kha

  committed
  06e0d78

  Copy full SHA for 06e0d78

Commits on Mar 20, 2018

• refactor(init/category/state): replace monad_state_lift with Haskell's MonadState

  Show description for 70167de
  

  Kha

  authored and

  leodemoura

  committed
  70167de

  Copy full SHA for 70167de

• refactor(init/category/functor): merge has_map into functor

  

  Kha

  authored and

  leodemoura

  committed
  bcbe5ec

  Copy full SHA for bcbe5ec

• chore(init/category/combinators): remove unnecessary monad.lift{n}

  

  Kha

  authored and

  leodemoura

  committed
  bac0f66

  Copy full SHA for bac0f66

• chore(init/category/transformers): remove now-unused monad_transformer class, rename to lift.lean

  

  Kha

  authored and

  leodemoura

  committed
  f4c2499

  Copy full SHA for f4c2499

• chore(changes.md): changelog

  

  Kha

  authored and

  leodemoura

  committed
  22d15ba

  Copy full SHA for 22d15ba

• refactor(init/category/state): replace monad_state with monad_state_lift

  

  Kha

  authored and

  leodemoura

  committed
  8c157eb

  Copy full SHA for 8c157eb

• refactor(init/category/lawful): unbundle lawful classes

  

  Kha

  authored and

  leodemoura

  committed
  940aca1

  Copy full SHA for 940aca1

• refactor(init/category/state): introduce monad_state

  Show description for 159b45c
  

  Kha

  authored and

  leodemoura

  committed
  159b45c

  Copy full SHA for 159b45c

• refactor(init/category): move monad laws into separate type classes defined after the tactic framework

  

  Kha

  authored and

  leodemoura

  committed
  1c68615

  Copy full SHA for 1c68615

• chore(init/category/transformers): move monad_transformer, monad_lift out of monad namespace, make universe polymorphic

  

  Kha

  authored and

  leodemoura

  committed
  63382cf

  Copy full SHA for 63382cf

Commits on Feb 28, 2018

• feat(frontends/lean/structure_cmd): allow implicitness infer annotation and parameters in field declaration

  Kha

  committed
  1abf873

  Copy full SHA for 1abf873

• feat(fronteds/lean/builtin_exprs): do notation: use overloadable bind instead of has_bind.bind

  Kha

  committed
  cf8dd9e

  Copy full SHA for cf8dd9e

Commits on Feb 19, 2018

• feat(library/time_task): print cumulative times on --profile

  

  Kha

  authored and

  leodemoura

  committed
  f247363

  Copy full SHA for f247363

Commits on Feb 2, 2018

• feat(frontends/lean/elaborator): structure notation: fall back to inferring superclasses

  

  Kha

  authored and

  leodemoura

  committed
  b3262d5

  Copy full SHA for b3262d5

• feat(frontends/lean/structure_cmd): make superclass fields inst implicit

  

  Kha

  authored and

  leodemoura

  committed
  86e231e

  Copy full SHA for 86e231e

• feat(frontends/lean/elaborator): structure instance notation: allow implicit fields

  

  Kha

  authored and

  leodemoura

  committed
  9f25cf6

  Copy full SHA for 9f25cf6

Commits on Jan 23, 2018

• refactor(library/io): make io easier to extend and use

  leodemoura

  committed
  0ad5497

  Copy full SHA for 0ad5497

• feat(util): allow some math alphanum symbol latin letter variations

  Show description for 1538615
  

  ratmice

  authored and

  leodemoura

  committed
  1538615

  Copy full SHA for 1538615

Commits on Jan 17, 2018

• feat(library/tactic/simplify): add simp!

  leodemoura

  committed
  368f17d

  Copy full SHA for 368f17d

• feat(library/tactic/simp_tactic): improve mk_simp_attr

  Show description for c195d7c
  leodemoura

  committed
  c195d7c

  Copy full SHA for c195d7c

Commits on Jan 15, 2018

• chore(doc/changes): document new leanpkg features

  Kha

  committed
  1d1e997

  Copy full SHA for 1d1e997

• fix(leanpkg): mandate path = "src"

  Show description for b354feb
  Kha

  committed
  b354feb

  Copy full SHA for b354feb

Commits on Jan 13, 2018

• feat(library/tactic/simplify): simp reduces c a_1 ... a_n = c b_1 ... b_n into a_1 = b_1 /\ ... /\ a_n = b_n

  leodemoura

  committed
  cebde17

  Copy full SHA for cebde17

Commits on Jan 12, 2018

• feat(library/init/meta/interactive): add interactive tactic subst_vars

  leodemoura

  committed
  58fce78

  Copy full SHA for 58fce78

• feat(library/init/meta/tactic): subst supports heterogeneous equalities that are actually homogeneous

  leodemoura

  committed
  5bad6d5

  Copy full SHA for 5bad6d5

• feat(library/tactic/simplify): simp reduces c_1 ... = c_2 ... to false

  leodemoura

  committed
  4bd314f

  Copy full SHA for 4bd314f

• feat(library/init/meta/interactive): add sorry interactive tactic (alias for admit).

  leodemoura

  committed
  c3d4a94

  Copy full SHA for c3d4a94

• feat(library/tactic): add support for auto params at simp tactic

  leodemoura

  committed
  c5df94e

  Copy full SHA for c5df94e

Commits on Jan 10, 2018

• doc(doc/changes): describe new "smart unfolding" feature

  leodemoura

  committed
  5cd0f25

  Copy full SHA for 5cd0f25

Commits on Jan 5, 2018

• feat(frontends/lean): add abbreviation command

  Show description for 587540f
  leodemoura

  committed
  587540f

  Copy full SHA for 587540f

Commits on Dec 15, 2017

• chore(library): remove out notation for out_param

  leodemoura

  committed
  91ff183

  Copy full SHA for 91ff183

Pagination

Previous

Next