Skip to content

Instantly share code, notes, and snippets.

@aqjune

aqjune/foo.lean

Created March 19, 2018 18:27
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 aqjune/da879565f6617b8b85f85362d5674983 to your computer and use it in GitHub Desktop.
Save aqjune/da879565f6617b8b85f85362d5674983 to your computer and use it in GitHub Desktop.
Download ZIP
monad
Raw
foo.lean
inductive any
| val : ∀ (α:Type), α → any
def bar (n:nat):option nat :=
return n
def foo:option any :=
do
dummy ← bar 10,
return (any.val nat 3)
/-
term
bar 10
has type
option ℕ : Type
but is expected to have type
option ?m_1 : Type 1
-/
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment