math-comp/algebra-tactics issues and pull requests

#46 - [WIP] Add an option: Set/Unset Algebra Tactics Debug

Pull Request - State: closed - Opened by pi8027 about 3 years ago - 7 comments

#46 - [WIP] Add an option: Set/Unset Algebra Tactics Debug

Pull Request - State: closed - Opened by pi8027 about 3 years ago - 7 comments

#45 - Compare structure instances rather than operators

Pull Request - State: closed - Opened by pi8027 about 3 years ago

#44 - Remove unused opaque definitions and add `Strategy expand`

Pull Request - State: closed - Opened by pi8027 about 3 years ago

#44 - Remove unused opaque definitions and add `Strategy expand`

Pull Request - State: closed - Opened by pi8027 about 3 years ago

#43 - Optimize tactics by locally locking ring operators (a better reimplementation of #41)

Pull Request - State: closed - Opened by pi8027 about 3 years ago - 1 comment

#43 - Optimize tactics by locally locking ring operators (a better reimplementation of #41)

Pull Request - State: closed - Opened by pi8027 about 3 years ago - 1 comment

#42 - Update CI

Pull Request - State: closed - Opened by pi8027 about 3 years ago

#41 - Optimize tactics by locally locking ring operators

Pull Request - State: closed - Opened by pi8027 about 3 years ago - 2 comments

#41 - Optimize tactics by locally locking ring operators

Pull Request - State: closed - Opened by pi8027 about 3 years ago - 2 comments

#40 - Support for `nat` ?

Issue - State: closed - Opened by amahboubi about 3 years ago - 3 comments

#40 - Support for `nat` ?

Issue - State: closed - Opened by amahboubi about 3 years ago - 3 comments

#39 - Reorganize Elpi files & CI for Coq 8.15

Pull Request - State: closed - Opened by pi8027 about 3 years ago

#39 - Reorganize Elpi files & CI for Coq 8.15

Pull Request - State: closed - Opened by pi8027 about 3 years ago

#38 - Remove zify_ring, zify_field, and ratify_field for the moment

Pull Request - State: closed - Opened by pi8027 about 3 years ago

#37 - Rename some definitions and constructors

Pull Request - State: closed - Opened by pi8027 about 3 years ago

#37 - Rename some definitions and constructors

Pull Request - State: closed - Opened by pi8027 about 3 years ago

#36 - Simpler quote predicates

Pull Request - State: closed - Opened by pi8027 about 3 years ago

#36 - Simpler quote predicates

Pull Request - State: closed - Opened by pi8027 about 3 years ago

#35 - Add zmodule.v

Pull Request - State: closed - Opened by pi8027 about 3 years ago

#35 - Add zmodule.v

Pull Request - State: closed - Opened by pi8027 about 3 years ago

#34 - Credits

Issue - State: closed - Opened by pi8027 over 3 years ago - 13 comments

#34 - Credits

Issue - State: closed - Opened by pi8027 over 3 years ago - 13 comments

#33 - [CI] add mathcomp:1.13.0-coq-(8.13|dev)

Pull Request - State: closed - Opened by pi8027 over 3 years ago

#33 - [CI] add mathcomp:1.13.0-coq-(8.13|dev)

Pull Request - State: closed - Opened by pi8027 over 3 years ago

#32 - Update OPAM package dependencies

Pull Request - State: closed - Opened by pi8027 over 3 years ago - 1 comment

#32 - Update OPAM package dependencies

Pull Request - State: closed - Opened by pi8027 over 3 years ago - 1 comment

#31 - Better post-processing of non-zero conditions

Pull Request - State: closed - Opened by pi8027 over 3 years ago

#31 - Better post-processing of non-zero conditions

Pull Request - State: closed - Opened by pi8027 over 3 years ago

#30 - Optimize constants in reified syntax trees

Pull Request - State: closed - Opened by pi8027 over 3 years ago

#30 - Optimize constants in reified syntax trees

Pull Request - State: closed - Opened by pi8027 over 3 years ago

#29 - Avoid repeating the same normalization in `field`

Pull Request - State: closed - Opened by pi8027 over 3 years ago - 2 comments

#28 - Fix Makefile

Pull Request - State: closed - Opened by pi8027 over 3 years ago

#28 - Fix Makefile

Pull Request - State: closed - Opened by pi8027 over 3 years ago

#27 - A performance issue with morphism detection

Issue - State: closed - Opened by pi8027 over 3 years ago - 3 comments

#27 - A performance issue with morphism detection

Issue - State: closed - Opened by pi8027 over 3 years ago - 3 comments

#26 - Fix some performance issues in reification

Pull Request - State: closed - Opened by pi8027 over 3 years ago - 2 comments

#26 - Fix some performance issues in reification

Pull Request - State: closed - Opened by pi8027 over 3 years ago - 2 comments

#25 - [CI] add mathcomp:(1.12.0|1.13.0)-coq-8.14

Pull Request - State: closed - Opened by pi8027 over 3 years ago

#25 - [CI] add mathcomp:(1.12.0|1.13.0)-coq-8.14

Pull Request - State: closed - Opened by pi8027 over 3 years ago

#24 - Some improvements

Pull Request - State: closed - Opened by pi8027 over 3 years ago

#24 - Some improvements

Pull Request - State: closed - Opened by pi8027 over 3 years ago

#23 - opam package

Issue - State: open - Opened by amahboubi over 3 years ago - 41 comments

#23 - opam package

Issue - State: open - Opened by amahboubi over 3 years ago - 41 comments

#22 - Semi-automate proofs of nonzero conditions in `field`

Pull Request - State: closed - Opened by pi8027 over 3 years ago - 3 comments
Labels: enhancement

#22 - Semi-automate proofs of nonzero conditions in `field`

Pull Request - State: closed - Opened by pi8027 over 3 years ago - 3 comments
Labels: enhancement

#21 - Fix simpl_PCond

Pull Request - State: closed - Opened by pi8027 over 3 years ago
Labels: bug

#21 - Fix simpl_PCond

Pull Request - State: closed - Opened by pi8027 over 3 years ago
Labels: bug

#20 - Semi-automating proofs of nonzero conditions in `field`

Issue - State: closed - Opened by pi8027 over 3 years ago - 2 comments
Labels: enhancement

#19 - Simplify non-zero conditions of the field tactic

Pull Request - State: closed - Opened by pi8027 over 3 years ago - 1 comment

#19 - Simplify non-zero conditions of the field tactic

Pull Request - State: closed - Opened by pi8027 over 3 years ago - 1 comment

#18 - Compare variables by conversion or keyed matching

Issue - State: open - Opened by pi8027 over 3 years ago - 6 comments
Labels: enhancement

#18 - Compare variables by conversion or keyed matching

Issue - State: open - Opened by pi8027 over 3 years ago - 6 comments
Labels: enhancement

#17 - Support converse rings

Issue - State: open - Opened by pi8027 over 3 years ago
Labels: enhancement

#17 - Support converse rings

Issue - State: open - Opened by pi8027 over 3 years ago
Labels: enhancement

#16 - Add support for additive functions and Z-modules

Pull Request - State: closed - Opened by pi8027 over 3 years ago
Labels: enhancement

#16 - Add support for additive functions and Z-modules

Pull Request - State: closed - Opened by pi8027 over 3 years ago
Labels: enhancement

#15 - Move basic definitions and lemmas about Z to mczify

Pull Request - State: closed - Opened by pi8027 over 3 years ago

#15 - Move basic definitions and lemmas about Z to mczify

Pull Request - State: closed - Opened by pi8027 over 3 years ago

#14 - Support additive functions and Z-modules

Issue - State: closed - Opened by pi8027 over 3 years ago
Labels: enhancement

#14 - Support additive functions and Z-modules

Issue - State: closed - Opened by pi8027 over 3 years ago
Labels: enhancement

#13 - Better handling of nonzero conditions in `field`

Issue - State: closed - Opened by pi8027 over 3 years ago - 2 comments

#13 - Better handling of nonzero conditions in `field`

Issue - State: closed - Opened by pi8027 over 3 years ago - 2 comments

#12 - Better support for product rings

Issue - State: open - Opened by pi8027 over 3 years ago
Labels: enhancement, help wanted

#11 - Support ring expressions with exponents

Issue - State: open - Opened by pi8027 over 3 years ago - 3 comments
Labels: enhancement

#11 - Support ring expressions with exponents

Issue - State: open - Opened by pi8027 over 3 years ago - 3 comments
Labels: enhancement

#10 - Update CI

Pull Request - State: closed - Opened by pi8027 over 3 years ago - 5 comments

#10 - Update CI

Pull Request - State: closed - Opened by pi8027 over 3 years ago - 5 comments

#9 - gitattributes: make GH color .elpi files as Prolog

Pull Request - State: closed - Opened by gares over 3 years ago

#9 - gitattributes: make GH color .elpi files as Prolog

Pull Request - State: closed - Opened by gares over 3 years ago

#8 - Morphisms

Pull Request - State: closed - Opened by pi8027 over 3 years ago - 1 comment

#8 - Morphisms

Pull Request - State: closed - Opened by pi8027 over 3 years ago - 1 comment

#7 - automatic introduction of hyps

Pull Request - State: closed - Opened by gares almost 4 years ago - 2 comments

#6 - Move elpi code to a .elpi file

Issue - State: closed - Opened by gares almost 4 years ago

#5 - Hypothesis handling

Issue - State: closed - Opened by pi8027 almost 4 years ago

#4 - Performance issue of reflection and support for morphisms

Issue - State: closed - Opened by pi8027 almost 4 years ago - 1 comment

#3 - Test suite

Pull Request - State: closed - Opened by pi8027 almost 4 years ago

#2 - port to coq-elpi 1.10

Pull Request - State: closed - Opened by gares almost 4 years ago - 15 comments

#1 - `exact<:` does not check the term is a proof of the current goal

Issue - State: closed - Opened by gares almost 4 years ago - 4 comments

GitHub / math-comp/algebra-tactics issues and pull requests