All pull requests

Pull requests

• fix: use reducible transparency when producing no_confusion_type and injectivity lemmas

  awaiting-review
  #812·eric-wieser opened Jun 14, 2023Member·

  ·
  10

• fix: use a less ambiguous encoding for relative imports

  #811·digama0 opened May 25, 2023Member·

  ·

• fix(frontends/lean/parser): start positions of trailing parser (NuD) nodes

  #785·digama0 opened Nov 18, 2022Member·

  ·
  2

• feat(frontends/lean/pp): use forall notation for all pi types from a Type to a Prop

  awaiting-review
  #770·kmill opened Sep 19, 2022Contributor·

  ·
  16

• FreeBSD patches

  #764·yurivict opened Sep 1, 2022Contributor·

  ·
  1

• feat(simp_lemmas): allow user congr lemma to have fixed parameters

  #709·kmill opened Mar 28, 2022Contributor·

  ·
  2

• feat(elaborator,pp): improvements to dot notation

  #708·kmill opened Mar 26, 2022Contributor·

  ·

• feat(frontends): local names in user-defined notation

  WIP
  #701·b-mehta opened Mar 15, 2022·

  ·

• Add module_info.get_all

  #645·eric-wieser opened Nov 2, 2021Member·

  ·
  5

• fix(library/type_context): do not enfore semireducible transparency in implicit arguments

  #556·gebner opened Mar 17, 2021Member·

  ·

• feat(library/init/core): allow lists of proofs

  #533·eric-wieser opened Feb 18, 2021Member·

  ·
  6

• feat(*): Log progress messages to stderr even when using json output on stdout

  #495·eric-wieser opened Oct 29, 2020Member·

  ·
  2

• fix(init/meta/converter/interactive): Do not allow rw to create ⊢ goals in conv mode

  WIP
  #475·eric-wieser opened Oct 8, 2020Member·

  ·
  5

• doc(tactic): add explanation of approx for unify

  #459·EdAyers opened Sep 2, 2020Member·

  ·
  1

• feat(?): Better support for prod in well_founded

  #414·eric-wieser opened Jul 28, 2020Member·

  ·
  1

• feat(meta/environment): the equations that lead to a given definition are now accessible in Lean code

  #393·cipher1024 opened Jul 16, 2020Contributor·

  ·
  5

• assumption?

  #281·jalex-stark opened May 27, 2020·

  ·
  25

• feat(library/init/meta/format): has_to_format α implies has_to_string α

  #231·JLimperg opened May 12, 2020Collaborator·

  ·
  1

• chore(library/init/data): constructive nat

  #171·Jack-Pumpkinhead opened Apr 1, 2020·

  ·

  · Lean 3.12
  4

• feat(tactic/lint): add some hooks to allow linting of proof scripts

  WIP
  #168·cipher1024 opened Apr 1, 2020Contributor·

  ·
  1

• Feature/vm dynload

  WIP
  #49·cipher1024 opened Jun 3, 2019Contributor·

  ·

• Add structs to FFI

  WIP
  #47·agentultra opened Jun 1, 2019Collaborator·

  ·

• WIP: cwd in environment objects

  WIP
  #43·cipher1024 opened May 17, 2019Contributor·

  ·

• feat(init/data/cached): Caching mechanism [WIP]

  WIP
  #35·digama0 opened May 10, 2019Member·

  ·