issues
search
affeldt-aist
/
monae
Monadic effects and equational reasonig in Coq
GNU Lesser General Public License v2.1
67
stars
11
forks
source link
issues
Newest
Newest
Most commented
Recently updated
Oldest
Least commented
Least recently updated
this example should maybe be moved
#142
affeldt-aist
opened
3 weeks ago
0
rm a couple of the functor
#141
affeldt-aist
closed
1 month ago
0
Subdirs
#140
affeldt-aist
closed
2 months ago
0
must `cnew` make its type argument implicit?
#139
affeldt-aist
opened
2 months ago
0
separate crun out of MonadTypedStore
#138
t6s
closed
2 months ago
3
remove unnecessary annotations
#137
garrigue
closed
2 months ago
0
isnt
#136
affeldt-aist
closed
2 months ago
0
revert hier.png
#135
t6s
closed
2 months ago
0
add a trivial model of MonadPlusArray (Module TrivialPlusArray)
#134
t6s
closed
2 months ago
1
::: for Cons in proofs
#133
garrigue
closed
2 months ago
0
ipartlE
#132
affeldt-aist
closed
2 months ago
0
start porting to MathComp 2
#131
affeldt-aist
closed
3 months ago
7
add cyclel_rdrop_self
#130
garrigue
closed
5 months ago
0
Typed store nier
#129
garrigue
closed
7 months ago
0
coqgen examples executable in monad_model
#128
t6s
closed
9 months ago
0
Wrt infotheo master
#127
affeldt-aist
closed
9 months ago
0
simplify proofs for cyclic lists
#126
garrigue
closed
10 months ago
0
More interesting example for cyclic list
#125
garrigue
closed
10 months ago
0
avoid hb.1.6.0
#124
affeldt-aist
closed
10 months ago
0
CI test
#123
t6s
closed
9 months ago
0
replace fsdist_convA by its generic version convA0
#122
t6s
opened
11 months ago
19
coercible
#121
affeldt-aist
closed
1 year ago
0
update readme
#120
affeldt-aist
closed
1 year ago
0
Fact_for63 evaluation
#119
garrigue
closed
1 year ago
0
Clarify eqtype
#118
garrigue
closed
1 year ago
0
add link to coq2023
#117
affeldt-aist
closed
1 year ago
0
Hide interface definitions
#116
garrigue
closed
1 year ago
0
add Restart and FromW
#115
garrigue
closed
1 year ago
0
make typed_store_model and example computable
#114
garrigue
closed
1 year ago
0
cputnewC
#113
affeldt-aist
closed
1 year ago
0
ML_universe as a mixin
#112
affeldt-aist
closed
1 year ago
0
Typed store monad wip
#111
affeldt-aist
closed
1 year ago
0
2023/6/30: SMCGlobal, SMCLocal and extract
#110
snowmantw
opened
1 year ago
1
cgetputC (wip) + wip
#109
affeldt-aist
closed
1 year ago
0
Ml type eq type
#108
affeldt-aist
closed
1 year ago
1
compat coq 8.17
#107
affeldt-aist
closed
1 year ago
0
define abstract category, impredicatively
#106
t6s
opened
1 year ago
0
add MonadTypedStore
#105
garrigue
closed
1 year ago
8
update wrt forthcoming infotheo
#104
affeldt-aist
closed
1 year ago
0
factory to buil monads from adjoint functors
#103
affeldt-aist
opened
1 year ago
0
document factories
#102
affeldt-aist
opened
1 year ago
0
More general bindret
#101
t6s
closed
1 year ago
1
add doi
#100
affeldt-aist
closed
1 year ago
0
trying to use infotheo_hb
#99
affeldt-aist
closed
1 year ago
2
compatibility with mathcomp 1.15.0
#98
affeldt-aist
closed
2 years ago
0
non forgetful inheritance detected
#97
affeldt-aist
opened
2 years ago
0
use HB in category.v and other dependent scripts
#96
t6s
closed
2 years ago
3
Compatibility with infotheo037
#95
affeldt-aist
closed
2 years ago
0
update figure
#94
AyumuSaito
closed
2 years ago
0
Intro equations
#93
AyumuSaito
closed
2 years ago
0
Next