leanprover lean3 issues

leanprover / lean3

Lean Theorem Prover

http://leanprover.github.io/

Apache License 2.0

2.15k stars 217 forks source link

issues

Newest

Newest Most commented Recently updated Oldest Least commented Least recently updated

build error: vm check failed: is_composite(o)

#2006 jwaldmann opened 4 years ago
1
rewrite cannot handle even the simplest of lemmas involving nat.rec

#2005 JasonGross opened 4 years ago
1
simp fails to handle recursors

#2004 JasonGross opened 4 years ago
2
Are there linux install instructions?

#2003 enricozb closed 4 years ago
1
Nested names confuse the typechecker

#2002 mrakgr closed 4 years ago
1
Autocomplete is incomplete

#2001 mrakgr closed 4 years ago
1
Feature/vm dynload

#2000 cipher1024 closed 5 years ago
0
Add structs support to FFI

#1999 agentultra closed 5 years ago
0
Fix a failing test (one more still fails, but you have a [TODO] in it)

#1998 khoek closed 5 years ago
1
fix(vm/get_cwd): add test for get_cwd

#1997 cipher1024 closed 5 years ago
1
Documentation for lean --server

#1996 whitequark opened 5 years ago
4
Universe metavariables and typeclass resolution failure

#1995 joehendrix opened 5 years ago
0
Add inductive no confusion

#1994 digama0 closed 5 years ago
1
[Question]: Proving false vs proving double negation

#1993 domfarolino closed 5 years ago
2
Angle brackets precidence

#1992 rspencer01 opened 5 years ago
0
Please have a cmake variable that controls if tests should be built

#1991 yurivict opened 5 years ago
0
Export contains tag #EZ that is not documented

#1990 huma23 closed 5 years ago
1
Remove relators and the transfer tactic

#1989 gebner closed 5 years ago
0
Deep recursion was detected at 'replace'

#1988 stop-cran closed 5 years ago
3
chore(.travis.yml): gpg key for new rvm maintainer

#1987 bryangingechen closed 5 years ago
1
fix(library/module_mgr): ignore '\r' changes

#1986 gebner closed 5 years ago
2
I cannot find native_compiler.h and some other header files in src folder while building

#1985 NeverLandFly closed 5 years ago
2
fix(library/coinductive_predicates): fix existential types

#1984 cipher1024 closed 5 years ago
4
fix(library/init):removed unused import

#1983 huma23 closed 5 years ago
1
repeated instance in init/algebra/field.lean

#1982 kckennylau closed 5 years ago
1
feat(leanpkg): add git branch tracking for dependencies

#1981 khoek closed 5 years ago
1
leanpkg fails if there's a space in the pathname to the binary

#1980 kevinsullivan opened 5 years ago
1
Import Isabelle theorems

#1979 mrmartin closed 5 years ago
1
fix(frontends/dependencies): ignore `.olean` files when listing depen…

#1978 cipher1024 closed 5 years ago
0
Add Coq-like "abort" tactic

#1977 kevinsullivan opened 5 years ago
4
fix(lean/bin/leanpkg*): handle spaces in paths

#1976 solson closed 5 years ago
2
leanpkg new returns failed to start child process

#1975 fstiffo opened 6 years ago
2
out of date files on bitbucket

#1974 holtzermann17 opened 6 years ago
0
leanpkg doesn't work on Windows when lean is copied to C:\Program Files\lean\

#1973 varosi closed 5 years ago
3
Seg fault on lean.exe

#1972 alisever opened 6 years ago
1
OSX binary depends on libgmp, missing by default

#1971 kevinsullivan opened 6 years ago
3
leanfmt: Lean code formatter

#1970 alok opened 6 years ago
2
Workaround for unsupported equality between type and constructor indices

#1969 evhub closed 6 years ago
5
algebraic data type vm check failed is_closure

#1968 joehendrix closed 6 years ago
2
doxygen: problems opening map file doc/html/inherit_graph_180.map for inclusion

#1967 andres-erbsen opened 6 years ago
0
gcc 8.1.1: trie.h:69:76: error: ‘this’ was not captured for this lambda function

#1966 andres-erbsen opened 6 years ago
4
GCC: ‘this’ was not captured for this lambda function

#1965 EdAyers closed 6 years ago
5
Can't find the output of exporting the Lean library in low level format.

#1964 ITervaNkYu opened 6 years ago
0
Meta program that traverses product expressions fails

#1963 kendroe closed 6 years ago
3
error with leanpkg

#1962 blairshi111 closed 5 years ago
1
subtype.eq has wrong signature

#1961 fgdorais opened 6 years ago
3
fix(doc/export_format): correct #DEF example and typos

#1960 andrejtokarcik closed 5 years ago
1
Typo in Tutorial

#1959 kevinsullivan closed 6 years ago
2
Segfault with monad inference

#1958 digama0 opened 6 years ago
0
Error with meta mutual defs

#1957 digama0 opened 6 years ago
0