Skip to content

Instantly share code, notes, and snippets.

@mbrcknl

mbrcknl/Norm.v

Created September 29, 2015 03:49
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save mbrcknl/2aeafb4551bed49a862d to your computer and use it in GitHub Desktop.
Save mbrcknl/2aeafb4551bed49a862d to your computer and use it in GitHub Desktop.
Download ZIP
Extending saturated sets to product types, alternative version
Raw
Norm.v
Fixpoint R (T:ty) (t:tm) {struct T} : Prop :=
has_type empty t T /\ halts t /\
match T with
| TBool => True
| TArrow T1 T2 => (forall s, R T1 s -> R T2 (tapp t s))
| TProd T1 T2 => exists t1, exists t2, t ==>* tpair t1 t2 /\ R T1 t1 /\ R T2 t2
end.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment