Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Benchmarks for the CwF and SplTC equivalence #193

Draft
wants to merge 2 commits into
base: master
Choose a base branch
from

Conversation

tvignon
Copy link
Contributor

@tvignon tvignon commented Jun 11, 2021

Some Benchmark for the CwF and SplTC equivalence, that contain mostly the common part of the two structure and some additional constructions :

  • The Ty presheaf
  • context extension
  • pi A
  • te A (the universal term of type A)
  • term equivalence between display version (one of them is not shown there but it already done in another PR, and could be adapted to make the equivalence with the middle structure)
  • q

For all of those benchmark there is 4 different setting :

  1. SplTC to CwF with SplTC as the reference one (the one given while the CwF is generated form the SplTC)
  2. CwF to SplTC with CwF as the reference one
  3. Middle Structure of the equivalence to CwF with the middle structure as the reference one
  4. Middle Structure of the equivalence to SplTC with the middle structure as the reference one

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

1 participant