leanprover/lean3

Issues

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

  #2006 opened 5 years ago by jwaldmann
  1

• simp fails to handle recursors

  #2004 opened 5 years ago by JasonGross
  2

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

  #2005 opened 5 years ago by JasonGross
  1

• Are there linux install instructions?

  #2003 opened 5 years ago by enricozb
  1

• Nested names confuse the typechecker

  #2002 opened 5 years ago by mrakgr
  1

• Autocomplete is incomplete

  #2001 opened 5 years ago by mrakgr
  1

• Deep recursion was detected at 'replace'

  #1988 opened 6 years ago by stop-cran
  3

• Export contains tag #EZ that is not documented

  #1990 opened 6 years ago by huma23
  1

• Documentation for lean --server

  #1996 opened 6 years ago by whitequark
  4

• Universe metavariables and typeclass resolution failure

  #1995 opened 6 years ago by joehendrix
  0

• [Question]: Proving false vs proving double negation

  #1993 opened 6 years ago by domfarolino
  2

• Angle brackets precidence

  #1992 opened 6 years ago by rspencer01
  0

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

  #1991 opened 6 years ago by yurivict
  0

• [feature] io.proc.fork

  #1953 opened 6 years ago by forked-from-1kasper
  0

• I cannot find native_compiler.h and some other header files in src folder while building

  #1985 opened 6 years ago by NeverLandFly
  2

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

  #1980 opened 6 years ago by kevinsullivan
  1

• error with leanpkg

  #1962 opened 6 years ago by blairshi111
  1

• Import Isabelle theorems

  #1979 opened 6 years ago by mrmartin
  1

• leanpkg doesn't work on Windows when lean is copied to C:\Program Files\lean\

  #1973 opened 6 years ago by varosi
  3

• Add Coq-like "abort" tactic

  #1977 opened 6 years ago by kevinsullivan
  4

• leanpkg new returns failed to start child process

  #1975 opened 6 years ago by fstiffo
  2

• out of date files on bitbucket

  #1974 opened 6 years ago by holtzermann17
  0

• GCC: ‘this’ was not captured for this lambda function

  #1965 opened 6 years ago by EdAyers
  5

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

  #1966 opened 6 years ago by andres-erbsen
  4

• OSX binary depends on libgmp, missing by default

  #1971 opened 6 years ago by kevinsullivan
  3

• Seg fault on lean.exe

  #1972 opened 6 years ago by alisever
  1

• Workaround for unsupported equality between type and constructor indices

  #1969 opened 6 years ago by evhub
  5

• leanfmt: Lean code formatter

  #1970 opened 6 years ago by alok
  2

• algebraic data type vm check failed is_closure

  #1968 opened 6 years ago by joehendrix
  2

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

  #1967 opened 6 years ago by andres-erbsen
  0

• Meta program that traverses product expressions fails

  #1963 opened 6 years ago by kendroe
  3

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

  #1964 opened 6 years ago by ITervaNkYu
  0

• subtype.eq has wrong signature

  #1961 opened 6 years ago by fgdorais
  3

• Typo in Tutorial

  #1959 opened 7 years ago by kevinsullivan
  2

• Segfault with monad inference

  #1958 opened 7 years ago by digama0
  0

• Error with meta mutual defs

  #1957 opened 7 years ago by digama0
  0

• Problem with `typed_expr`

  #1954 opened 7 years ago by johoelzl
  0

• silent overflow with large integers

  #1956 opened 7 years ago by kbuzzard
  0

• nat.pow is not right-associative

  #1951 opened 7 years ago by kbuzzard
  1

• assertion violation when using rfl to define instance

  #1952 opened 7 years ago by kbuzzard
  1

• Build broken by last commit

  #1946 opened 7 years ago by kim-em
  0

• Lean assertion violation

  #1942 opened 7 years ago by kim-em
  0

• unknown declaration 'B.mk.inj_eq._aux_1'

  #1943 opened 7 years ago by kim-em
  2

• ematch fails when there are two instance arguments which are different types of a type family

  #1940 opened 7 years ago by kim-em
  2

• bug with pp.implicit and structure fields

  #1922 opened 7 years ago by kim-em
  0

• Adding type class instances in tactic mode doesn't work anymore

  #1920 opened 7 years ago by johoelzl
  12

• Build shouldn't copy files into the source directory

  #1918 opened 7 years ago by nunoplopes
  4

• assertion violation

  #1930 opened 7 years ago by kim-em
  0

• Name collision between fields and parameters in struct declaration

  #1928 opened 7 years ago by Rotsor
  1

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

  #1921 opened 7 years ago by cipher1024
  1