Skip to content
This repository has been archived by the owner on Oct 14, 2023. It is now read-only.

Issues: leanprover/lean3

58 Open 1,066 Closed
58 Open 1,066 Closed
Author
Filter by author
Loading
Label
Filter by label
Loading
Use alt + click/return to exclude labels
or ⇧ + click/return for logical OR
Projects
Filter by project
Loading
Milestones
Filter by milestone
Loading
Assignee
Filter by who’s assigned
Sort
Sort by
Newest Oldest Most commented Least commented Recently updated Least recently updated Best match
Most reactions
👍 👎 😄 🎉 😕 ❤️ 🚀 👀

Issues list

build error: vm check failed: is_composite(o)
#2006 opened Oct 31, 2019 by jwaldmann
1
rewrite cannot handle even the simplest of lemmas involving nat.rec
#2005 opened Oct 30, 2019 by JasonGross
1 task done
1
simp fails to handle recursors
#2004 opened Oct 30, 2019 by JasonGross
1 task done
2
Documentation for lean --server
#1996 opened Mar 28, 2019 by whitequark
1 task done
4
Universe metavariables and typeclass resolution failure
#1995 opened Mar 13, 2019 by joehendrix
1 task done
Angle brackets precidence
#1992 opened Feb 1, 2019 by rspencer01
1 task done
Please have a cmake variable that controls if tests should be built
#1991 opened Jan 23, 2019 by yurivict
leanpkg fails if there's a space in the pathname to the binary
#1980 opened Nov 7, 2018 by kevinsullivan
1
Add Coq-like "abort" tactic
#1977 opened Oct 8, 2018 by kevinsullivan
4
leanpkg new returns failed to start child process
#1975 opened Oct 4, 2018 by fstiffo
2
out of date files on bitbucket
#1974 opened Sep 28, 2018 by holtzermann17
Seg fault on lean.exe
#1972 opened Sep 2, 2018 by alisever
1
OSX binary depends on libgmp, missing by default
#1971 opened Aug 30, 2018 by kevinsullivan
3
leanfmt: Lean code formatter
#1970 opened Aug 29, 2018 by alok
2
doxygen: problems opening map file doc/html/inherit_graph_180.map for inclusion
#1967 opened Aug 8, 2018 by andres-erbsen
1 task done
gcc 8.1.1: trie.h:69:76: error: ‘this’ was not captured for this lambda function
#1966 opened Aug 8, 2018 by andres-erbsen
1 task done
4
Can't find the output of exporting the Lean library in low level format.
#1964 opened Jul 30, 2018 by ITervaNkYu
1
subtype.eq has wrong signature
#1961 opened Jul 5, 2018 by fgdorais
1 task done
3
Segfault with monad inference
#1958 opened Apr 17, 2018 by digama0
1 task done
Error with meta mutual defs
#1957 opened Apr 17, 2018 by digama0
1 task done
Name collision between fields and parameters in struct declaration
#1928 opened Feb 17, 2018 by Rotsor
1 task done
1
expr.pis produces a type incorrect expr out of a type correct one
#1921 opened Feb 4, 2018 by cipher1024
1 task done
1
Limit the amount of error messages
#1912 opened Jan 24, 2018 by Kha
to_expr does not check that referenced parameters are in scope
#1908 opened Jan 21, 2018 by cipher1024
1 task done
apply ignores reducibility hints in some cases
#1906 opened Jan 12, 2018 by digama0
1 task done
ProTip! Find all open issues with in progress development work with linked:pr.