issues
search
bedrocksystems
/
coq-lens
Lenses in Coq
Other
17
stars
6
forks
source link
issues
Newest
Newest
Most commented
Recently updated
Oldest
Least commented
Least recently updated
invalid URL in opam package ?
#24
fblanqui
opened
3 months ago
0
Notation `_ & _` interferes with Coq's `sigT` notation
#23
swasey
closed
5 months ago
2
error installing coq-lens with opam
#22
rhz
closed
5 months ago
1
Support Coq 8.14 and 8.15
#21
Blaisorblade
closed
2 years ago
1
`lens` combinator?
#20
quinn-dougherty
opened
2 years ago
1
Need support coq 8.13
#19
NanachiKyubey
closed
5 months ago
1
Bugfix: add missing Bind Scope
#18
Blaisorblade
closed
3 years ago
0
Tweak lens notation.
#17
swasey
closed
3 years ago
0
Lens notations
#16
gstew5
closed
3 years ago
1
DRAFT: Make code compile with coq 8.13.
#15
Janno
closed
3 years ago
0
more documentation, addressed Gordon's suggestion
#14
aa755
closed
2 years ago
1
ported to Coq 8.12 (metacoq syntax changed)
#13
aa755
closed
3 years ago
1
preliminary lens notations
#12
gmalecha
opened
4 years ago
0
`From Lens Require Lens TC.TC.` lenses breaks ssreflect rewrite syntax `-!` *transitively*
#11
Janno
closed
5 months ago
4
thinking about the laws with lens families
#10
gmalecha
opened
4 years ago
0
Lens notations
#9
gmalecha
closed
5 months ago
1
Lens laws
#8
gmalecha
opened
4 years ago
0
ported to 8.11. added the genLensN function
#7
aa755
closed
4 years ago
0
warn when no projections are found.
#6
gmalecha
closed
5 years ago
0
lens generation silently fails when primitive projections not set
#5
aa755
closed
5 years ago
2
Switch to the Haskell definition
#4
gmalecha
closed
4 years ago
1
Prisms?
#3
gmalecha
opened
6 years ago
0
Polymorphic lenses
#2
gmalecha
opened
6 years ago
0
Universe polymorphism
#1
gmalecha
opened
6 years ago
0