search

meta-introspector / UniMath

This coq library aims to formalize a substantial body of mathematics using the univalent point of view.
http://unimath.org/
Other
0 stars 0 forks source link

metacoq #2

Open jmikedupont2 opened 8 months ago

jmikedupont2 commented 8 months ago

Significance: this is the first extraction of unimath into data that can be fed back into unimath as values

  1. added metacoq to unimath
  2. recursivly extracted first three layers

  3. applied ppx-introspector to extract data https://github.com/meta-introspector/ppxlib-simple-example/tree/feature/reworkHack/metacoq

  4. saved dump of output