Skip to content

Instantly share code, notes, and snippets.

@kbuzzard

kbuzzard/some0.lean

Created June 29, 2018 22:20
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 kbuzzard/455709bfd5d8fed57f5e4321481adf5b to your computer and use it in GitHub Desktop.
Save kbuzzard/455709bfd5d8fed57f5e4321481adf5b to your computer and use it in GitHub Desktop.
Download ZIP
What is `some 0`?
Raw
some0.lean
definition X := some 0
#check X
#check ℕ
#check option
#check some
#check @some
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment