Skip to content

Instantly share code, notes, and snippets.

@koba-e964

koba-e964/lean-universe-polymorphism-unification-failure.lean

Created September 6, 2017 15:23
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 koba-e964/0ae8f1bbe16ae88ca8c27ecb33531d23 to your computer and use it in GitHub Desktop.
Save koba-e964/0ae8f1bbe16ae88ca8c27ecb33531d23 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
lean-universe-polymorphism-unification-failure.lean
universe u
constant t: Sort u
constant f: t -> t
constant x: t
lemma test: x = x := by reflexivity
lemma test2: f x = f x := by reflexivity
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment