Bas Spitters
Bas Spitters
I imagine that one would somehow like to compare with the stdlibs of ocaml and haskell. The Vocal project aims to provide a verified basic library for ocaml. https://vocal.lri.fr/ https://hal.inria.fr/hal-01561094...
I guess the only way to find out is to ask @backtracking .
I was thinking about this project by @jwiegly https://github.com/jwiegley/coq-haskell and @swierich 's project has a similar aim. https://github.com/antalsz/hs-to-coq
Eelis van der Weegen once wrote: http://www.eelis.net/coqindent/ "coqindent is a small crude Python script that indents Coq proof scripts. It works by scanning coqtop's output for "# subgoals" strings and...
@robbertkrebbers @letouzey
Prop is an artifact from the time that Coq was geared towards program extraction. HoTT's hProp (i.e. with unique choice and propositional extensionality) would be closer to the usual intuition....
@gmalecha I wonder who is using Prop without wanting to use UIP too.
@ppedrot Yes, I meant PI. Indeed, I use impredicative set in some of my programming exercises for Fw, but I wouldn't put it in stdlib2.
It would be good to record an intended semantics. E.g. the set model and a homotopic model.
There is a reference to Coquand's model of MLTT+sProp here. However, they don't work out the differences between Coq and MLTT. https://dl.acm.org/doi/10.1145/3290316