Encodings

The encoding is a set of lambdapi files in encoding/ that define axioms allowing to type check PVS terms and propositions.

lhol

Simple Type theory expressed as a PTS commonly named λHOL

pvs_cert

Explicit predicate subtyping

tuple

Non dependents, lengthed tuples. Can also be seen as a non dependent version of de Bruijn telescopes.

logical

Locical connectives

eq

Equality =\, t\, u with elimination principle

coercions

Define coercions to implement implicit predicate subtyping

extra

More definitions and tools

alt

Alternate definitions

examples

Some example specification