Skip to content

Instantly share code, notes, and snippets.

@tomprince

tomprince/canon1.v

Created April 18, 2011 14:42
Show Gist options

  • Select an option

    Learn more about clone URLs
  • Save tomprince/925476 to your computer and use it in GitHub Desktop.

Select an option

Learn more about clone URLs
Save tomprince/925476 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
canon1.v
Section test.
Context (T U: Type) .
Record rec := { x :> Type}.
Canonical Structure t := Build_rec T.
Canonical Structure u := Build_rec U.
Context {f : forall {r:rec}, (x r) -> unit}.
Check (f T).
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment