pycoq

pycoq copied to clipboard

codesmell: breaks when `import pycoq` is omitted even tho `pycoq` is not invoked.

1

when I comment out `import pycoq`, I get ``` dune exec -- python3 _build/default/examples/add_commutative.py Traceback (most recent call last): File "_build/default/examples/add_commutative.py", line 2, in import coq ModuleNotFoundError: No module named...

quinn-dougherty

goal: a jupyter build, probably docker image.

1

let the user use `pycoq` in a notebook.

quinn-dougherty

We need to create documentation; first thing to understand is what tools are used in the Python world.

ejgallego

This is a general issue to discuss laziness and sharing w.r.t. the seralization of objects. A motivating example is the following usual Coq snippet: ``` type a = { foo...

ejgallego

As of today, OCaml types are encoded by `ppx_python` as more or less straight lists. This is OK, however not very idiomatic, and limited in some cases (maybe GADTs?) On...

ejgallego