Skip to content

Instantly share code, notes, and snippets.

@edoput

edoput/correctness.v

Created June 14, 2019 10:03
Show Gist options
  • Save edoput/99cf0bc840444f5d5b6b7b7978331fec to your computer and use it in GitHub Desktop.
Save edoput/99cf0bc840444f5d5b6b7b7978331fec to your computer and use it in GitHub Desktop.
Download ZIP
Correctness of the type checker
Raw
correctness.v
Lemma correctness : (forall (gamma : environment) (t : term) (tt : type),
has_type gamma t tt -> (type_check gamma t) = Some({ tt | has_type gamma t tt})).
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment