abella-prover abella issues

abella-prover / abella

An interactive theorem prover based on lambda-tree syntax

https://abella-prover.org/

GNU General Public License v3.0

90 stars 18 forks source link

issues

Newest

Newest Most commented Recently updated Oldest Least commented Least recently updated

Suspend declarations and Imports

#159 ThatDaleMiller opened 1 week ago
1
Proving false when using import-with

#158 ThatDaleMiller closed 1 month ago
3
Fix missing error locations

#157 wikku closed 3 months ago
1
Running Abella in the browser

#156 tausbn opened 6 months ago
3
Variable confusion/ill typed terms with higher-order terms

#155 wikku closed 4 months ago
11
Build fails: Error (warning 70 [missing-mli]): Cannot find interface file.

#154 yurivict closed 1 month ago
8
Simultaneous replacements broken in `Import ... with`

#153 chaudhuri closed 7 months ago
0
SOUNDNESS BUG: `Import ... with` does not check that the replacements are distinct

#152 chaudhuri closed 10 months ago
0
Support bytecode-only target for 32-bit platforms like powerpc

#151 barracuda156 closed 4 months ago
43
fix: damf context elements from local imports

#150 innofarah closed 1 year ago
2
fix: locally imported lemmas not being tracked (or failure to publish when trying to link to those lemmas).

#149 innofarah closed 1 year ago
3
[regression in 2.0.8] Error: Version 3.11 of the dune language is not supported.

#148 yurivict closed 1 year ago
5
Higher-order constants can be used to prove false

#147 chaudhuri closed 1 year ago
6
false can be proved

#146 cu1ch3n closed 1 year ago
6
Automatically generated hypotheses conflict with user-named ones

#145 lambdacalculator closed 1 year ago
0
Weird interaction between subordination and schematic theorems

#144 chaudhuri opened 1 year ago
0
Unification failure applying generic theorem

#143 RandomActsOfGrammar closed 1 year ago
6
Unexpected failure of generic type unification

#142 yvting opened 2 years ago
0
POLA violation on conjunctive theorems

#141 chaudhuri opened 2 years ago
0
Feature request: allow repetitions of definitions and theorems

#140 chaudhuri closed 1 year ago
2
Repeated Kind is OK, but repeated Type is not

#139 chaudhuri opened 2 years ago
0
Adds tests into dune build system

#138 cjohnson19 closed 2 years ago
1
Notify/warn the user when a `skip` is used in a .thm file?

#137 innofarah closed 2 years ago
1
Basic tactical support

#136 JimmyZJX opened 3 years ago
3
Add `unfold named_clause with ...` form

#135 chaudhuri opened 3 years ago
0
The Reprove top-level command

#134 JimmyZJX opened 3 years ago
0
Feature request: multiple proofs of the same theorem

#133 chaudhuri opened 3 years ago
0
Abella 2.0.7 to be made compatible with OCaml 4.08.0+

#132 chaudhuri closed 3 years ago
1
Handling equalities is way too painful

#131 silene opened 3 years ago
10
Ill-typed code with schematic polymorphism

#130 RandomActsOfGrammar opened 3 years ago
2
case fails to normalize object sequents

#129 silene closed 3 years ago
5
Constants allowed in types inside type constructors

#128 RandomActsOfGrammar closed 4 years ago
0
Asserting implication sets premise equalities

#127 RandomActsOfGrammar closed 4 years ago
2
Website is offline

#126 cyberglot closed 4 years ago
2
Fix for recent OCaml versions.

#125 pthariensflame closed 4 years ago
0
Abella 2.0.6 does not work well with PG

#124 kyagrd closed 4 years ago
5
2.0.6 won't build with ocaml-4.08.1

#123 Ponce closed 4 years ago
2
Feature: tactic `applys` as a handy version of `apply`

#122 JimmyZJX opened 5 years ago
4
Basic tactical support

#121 JimmyZJX opened 5 years ago
1
incorrect reuse of name in generated case

#120 south163 opened 5 years ago
1
`unfold id n` tactic

#119 lambdacalculator opened 5 years ago
1
Search hangs

#118 lambdacalculator opened 5 years ago
6
Search is very slow since 2.0.6

#117 chaudhuri opened 5 years ago
0
Implement compute

#116 chaudhuri opened 5 years ago
0
Automatically compile Import does not work properly on Windows

#115 JimmyZJX opened 5 years ago
5
substitution in equality

#114 htzh opened 5 years ago
8
Trivial assertions do not unwind state

#113 chaudhuri closed 5 years ago
0
Feature request: explicitly specify * and @ by user

#112 JimmyZJX opened 5 years ago
3
Move from ocamlbuild to dune

#111 chaudhuri closed 5 years ago
1
Confusion between regular and nominal constants in eta-contraction

#110 yvting closed 5 years ago
0