Skip to content

Instantly share code, notes, and snippets.

@mbrcknl

mbrcknl/Norm.v

Created September 29, 2015 03:36
Show Gist options
  • Save mbrcknl/737cb4b26edc0b6136f7 to your computer and use it in GitHub Desktop.
Save mbrcknl/737cb4b26edc0b6136f7 to your computer and use it in GitHub Desktop.
Download ZIP
Extending saturated sets to product types
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 => R T1 (tfst t) /\ R T2 (tsnd t)
end.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment