Skip to content

Instantly share code, notes, and snippets.

@kevinsullivan

kevinsullivan/empty.lean Secret

Created April 24, 2017 06:05
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 kevinsullivan/cebe8d66ba026daf2997fbaeb73bce29 to your computer and use it in GitHub Desktop.
Save kevinsullivan/cebe8d66ba026daf2997fbaeb73bce29 to your computer and use it in GitHub Desktop.
Download ZIP
The empty abstract data type has no_fun
Raw
empty.lean
namespace lfp
inductive empty: Type
definition no_fun: empty -> empty :=
fun e: empty, e
end lfp
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment