Andromedans andromeda issues

Andromedans / andromeda

A proof assistant for general type theories

http://www.andromeda-prover.org/

Other

297 stars 34 forks source link

issues

Newest

Newest Most commented Recently updated Oldest Least commented Least recently updated

Transformations basic

#545 anjapetkovic closed 1 month ago
1
Linear patterns

#544 anjapetkovic closed 1 month ago
0
bug fix in metavar args in rewrite + tests

#543 anjapetkovic closed 3 years ago
0
Eqchk error reports

#542 anjapetkovic closed 3 years ago
0
fixed normalizing types before extensionality phase

#541 anjapetkovic closed 4 years ago
0
dispatching on arguments that bind variables

#540 mikeshulman opened 4 years ago
0
Automatic principal arguments in eqchk

#539 anjapetkovic opened 4 years ago
0
Failed assertion

#538 mikeshulman opened 4 years ago
1
Provide an interface for unchecked nested converts.

#537 andrejbauer closed 4 years ago
0
a global handler for holes in prelude.

#536 anjapetkovic closed 4 years ago
0
cleanup of assumption sets in rewrite

#535 anjapetkovic closed 4 years ago
0
Rewrite

#534 anjapetkovic closed 4 years ago
0
Printing of local contexts in argument position is reversed

#533 haselwarter opened 4 years ago
0
Runtime exceptions are printed in wrong environment

#532 haselwarter opened 4 years ago
0
Eqchk abstracted constructors

#531 anjapetkovic closed 4 years ago
0
Local equations in eqchk and exceptions

#530 anjapetkovic closed 4 years ago
0
Add AML support for creating meta variables.

#529 andrejbauer closed 4 years ago
0
printing types of terms in derivations

#528 anjapetkovic closed 4 years ago
0
Fun patterns

#527 anjapetkovic closed 4 years ago
0
Implement general boundaries in premises.

#526 andrejbauer closed 4 years ago
2
Allow patterns in `fun`

#525 andrejbauer closed 4 years ago
0
Work around a sedlex bug resulting in an uncaught exception

#524 haselwarter closed 4 years ago
0
Simplify travis CI scripts, use opam as per the website

#523 haselwarter closed 4 years ago
0
Work around a sedlex bug resulting in an uncaught exception

#522 haselwarter closed 4 years ago
0
`open` should be forgotten at the end of a module

#521 andrejbauer opened 4 years ago
3
No atoms in rules

#520 andrejbauer closed 4 years ago
0
Better error messages for `context` and otherwise, close #489

#519 andrejbauer closed 4 years ago
0
Require modules at most one.

#518 andrejbauer closed 4 years ago
0
added ? to eq pattern variables

#517 anjapetkovic closed 4 years ago
0
Nullary derivations and rule applications.

#516 andrejbauer closed 4 years ago
0
Tag pattern meta-variables with questionmarks.

#515 andrejbauer closed 4 years ago
0
Simplify type of `coerce` and `equal_type`, close #510

#514 andrejbauer closed 4 years ago
0
sedlex version important

#513 anjapetkovic closed 4 years ago
0
Improve the `eq` module

#512 andrejbauer opened 4 years ago
0
Require each module at most once

#511 andrejbauer closed 4 years ago
0
Fix `coerce`

#510 andrejbauer closed 4 years ago
0
Print types of terms

#509 anjapetkovic closed 4 years ago
0
Have congruence rules handle atoms as well.

#508 andrejbauer closed 4 years ago
0
Fix topcomp printing

#507 haselwarter closed 4 years ago
0
Clean up theories a bit.

#506 andrejbauer closed 4 years ago
0
Tuareg-based Andromeda mode

#505 andrejbauer closed 4 years ago
0
Introduce the `a ≡ b : T by p` and `A ≡ B by q` notations.

#504 andrejbauer closed 4 years ago
0
fixed MLTT example, so that the equality checker is used

#503 anjapetkovic closed 4 years ago
0
Print `by` instead of `as`.

#502 andrejbauer closed 4 years ago
0
Eqchk conversion

#501 andrejbauer closed 4 years ago
1
Fix operation continuations

#500 andrejbauer closed 4 years ago
0
Replace `as` in `A == B as p` with `by`.

#499 andrejbauer closed 4 years ago
0
Strong normalization

#498 andrejbauer closed 4 years ago
0
some tests for equality checker

#497 anjapetkovic closed 4 years ago
1
Rules as derivations

#496 andrejbauer closed 4 years ago
0