Issues

• build error: vm check failed: is_composite(o)

  leanprover/lean3#2006 · Filter by author jwaldmann opened on Oct 31, 2019
  1

• rewrite cannot handle even the simplest of lemmas involving nat.rec

  leanprover/lean3#2005 · Filter by author JasonGross opened on Oct 30, 2019
  1

• simp fails to handle recursors

  leanprover/lean3#2004 · Filter by author JasonGross opened on Oct 30, 2019
  2

• Documentation for lean --server

  leanprover/lean3#1996 · Filter by author whitequark opened on Mar 28, 2019
  4

• Universe metavariables and typeclass resolution failure

  leanprover/lean3#1995 · Filter by author joehendrix opened on Mar 13, 2019

• Angle brackets precidence

  leanprover/lean3#1992 · Filter by author rspencer01 opened on Feb 1, 2019

• Please have a cmake variable that controls if tests should be built

  leanprover/lean3#1991 · Filter by author yurivict opened on Jan 23, 2019

• leanpkg fails if there's a space in the pathname to the binary

  leanprover/lean3#1980 · Filter by author kevinsullivan opened on Nov 7, 2018
  1

• Add Coq-like "abort" tactic

  leanprover/lean3#1977 · Filter by author kevinsullivan opened on Oct 8, 2018
  4

• leanpkg new returns failed to start child process

  leanprover/lean3#1975 · Filter by author fstiffo opened on Oct 4, 2018
  2

• out of date files on bitbucket

  leanprover/lean3#1974 · Filter by author holtzermann17 opened on Sep 28, 2018

• Seg fault on lean.exe

  leanprover/lean3#1972 · Filter by author alisever opened on Sep 2, 2018
  1

• OSX binary depends on libgmp, missing by default

  leanprover/lean3#1971 · Filter by author kevinsullivan opened on Aug 30, 2018
  3

• leanfmt: Lean code formatter

  leanprover/lean3#1970 · Filter by author alok opened on Aug 29, 2018
  2

• doxygen: problems opening map file doc/html/inherit_graph_180.map for inclusion

  leanprover/lean3#1967 · Filter by author andres-erbsen opened on Aug 8, 2018

• gcc 8.1.1: trie.h:69:76: error: ‘this’ was not captured for this lambda function

  leanprover/lean3#1966 · Filter by author andres-erbsen opened on Aug 8, 2018
  4

• Can't find the output of exporting the Lean library in low level format.

  leanprover/lean3#1964 · Filter by author ITervaNkYu opened on Jul 30, 2018

• subtype.eq has wrong signature

  leanprover/lean3#1961 · Filter by author fgdorais opened on Jul 5, 2018
  3

• Segfault with monad inference

  leanprover/lean3#1958 · Filter by author digama0 opened on Apr 17, 2018

• Error with meta mutual defs

  leanprover/lean3#1957 · Filter by author digama0 opened on Apr 17, 2018

• Name collision between fields and parameters in struct declaration

  leanprover/lean3#1928 · Filter by author Rotsor opened on Feb 17, 2018
  1

• expr.pis produces a type incorrect expr out of a type correct one

  leanprover/lean3#1921 · Filter by author cipher1024 opened on Feb 4, 2018
  1

• Limit the amount of error messages

  leanprover/lean3#1912 · Filter by author Kha opened on Jan 24, 2018

• to_expr does not check that referenced parameters are in scope

  leanprover/lean3#1908 · Filter by author cipher1024 opened on Jan 21, 2018

• apply ignores reducibility hints in some cases

  leanprover/lean3#1906 · Filter by author digama0 opened on Jan 12, 2018