package coq-ptsatr

  1. Overview
  2. Homepage

Description

Formalization of the proof that PTS and PTS with judgmental equality (PTSe) are equivalent. With this equivalence, we are able to derive all the meta-theory of PTSe, like Pi-injectivity or Subject Reduction.

Dependencies (2)

  1. coq >= "8.5" & < "8.6~"
  2. ocaml

Dev Dependencies

None

Used by (1)

  1. coq-ptsf < "8.6.0"

Conflicts

None

Rocq

Interactive Theorem Prover