issues
search
coq-community
/
metaprogramming-rosetta-stone
A rosetta stone for metaprogramming in Coq, with different examples of tactics, plugins, etc implemented in different metaprogramming languages [maintainer=@yforster]
MIT License
17
stars
5
forks
source link
issues
Newest
Newest
Most commented
Recently updated
Oldest
Least commented
Least recently updated
New example with comments: ho_equalities, written in Ltac, Ltac2 and coq-elpi
#21
louiseddp
opened
11 months ago
2
Autoinduct documentation improvement
#20
NeuralCoder3
opened
1 year ago
0
CI for autoinduct
#19
yforster
closed
1 year ago
0
add basic meta.yml, generate README.md from templates
#18
palmskog
opened
1 year ago
5
A simplification tactic for Z-module equations, specific to Z
#17
pi8027
opened
1 year ago
0
Change reflexive -> reflective
#16
gmalecha
closed
1 year ago
3
Follow-up meta task and notes
#15
tlringer
opened
1 year ago
9
adding metacoq autoinduct steps 2 and 3
#14
Tvallejos
closed
1 year ago
0
A reflexive tactic for Z-modules (commutative groups), specific to Z
#13
pi8027
closed
1 year ago
2
Autoinduct, document Ltac1 version in README
#12
tlringer
closed
1 year ago
0
Autoinduct, document OCaml version in README
#11
tlringer
closed
1 year ago
0
Autoinduct, add more tests
#10
tlringer
opened
1 year ago
1
Autoinduct, Ltac, switch between versions depending on input
#9
tlringer
opened
1 year ago
0
Autoinduct, OCaml, switch between versions depending on input
#8
tlringer
closed
1 year ago
0
Loosen autoinduct OCaml assumptions when possible; otherwise document
#7
tlringer
opened
1 year ago
0
Loosen autoinduct Ltac assumptions if possible; otherwise document
#6
tlringer
opened
1 year ago
0
Real simplifier: editorial changes + typo fixes
#5
MSoegtropIMC
closed
1 year ago
0
Autoinduct, OCaml, Part 3
#4
tlringer
closed
1 year ago
0
Autoinduct, Ltac, Part 3
#3
tlringer
opened
1 year ago
0
Autoinduct, Ltac, Part 2
#2
tlringer
opened
1 year ago
0
Update README.md
#1
gares
closed
1 year ago
0