Commit f85563e7 authored by Raphael Cauderlier's avatar Raphael Cauderlier

[doc] Small fix

parent c8e706c3
......@@ -591,9 +591,7 @@ and =c2= proves =C= in context =G= with an extra variable =x= of type
The file [[./meta/eqcert.dk][meta/eqcert.dk]] defines a few certificate combinators to
reason about equality:
- =eqcert.match_equality : fol.prop -> (A : fol.type -> fol.term A ->
fol.term A -> cert.certificate) -> cert.certificate ->
cert.certificate=
- =eqcert.match_equality : fol.prop -> (A : fol.type -> fol.term A -> fol.term A -> cert.certificate) -> cert.certificate -> cert.certificate=
- =eqcert.reflexivity : cert.certificate=
- =eqcert.symmetry : cert.certificate -> cert.certificate=
- =eqcert.transitivity : A : fol.type -> fol.term A -> cert.certificate -> cert.certificate -> cert.certificate=
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment