Damien Pous

status of example files in the library

2

@damien-pous : a note on our "smoke test kit" (a quick check Coq Platform does to check if all packages are installed properly): I selected the files `compiler_opts.v` and `imp.v`...

bounding box of an image

2

Hi, First of all, thanks for this nice library! I'm wondering if there is (or could be) a way to compute the "bounding box" of an image. I.e., the least...

I have a case where HB.saturate on a given key hangs: https://github.com/damien-pous/partial-orders/blob/eb3b26da87156f8ecab28169e7b190365403c194/theories/lattice.v#L15 It's rather hard to minimise; the strange thing is that HB.saturate on a rather similar key (monotone functions...

It seems there is no way to saturate the key (forall _,_). Cf. https://github.com/damien-pous/partial-orders/blob/eb3b26da87156f8ecab28169e7b190365403c194/theories/lattice.v#L17 Merci @CohenCyril ;)