Commit 6eb956d4 authored by François Thiré's avatar François Thiré

Add an encoding of STT with a new folder for theories.

parent 325ca643
#NAME stt.
type : Type.
prop : type.
arrow : type -> type -> type.
def eta : type -> Type.
forall : A:type -> (eta A -> eta prop) -> eta prop.
impl : eta prop -> eta prop -> eta prop.
def eps : eta prop -> Type.
[a, b] eta (arrow a b) --> eta a -> eta b.
[A, f] eps (forall A f) --> x:eta A -> eps (f x).
[l, r] eps (impl l r) --> eps l -> eps r.
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