Skip to content

Instantly share code, notes, and snippets.

@piyush-kurur

piyush-kurur/constructors and module variables

Created March 21, 2018 07:08
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 piyush-kurur/27d0778904e9ff86c84124f7bf90bf56 to your computer and use it in GitHub Desktop.
Save piyush-kurur/27d0778904e9ff86c84124f7bf90bf56 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
constructors and module variables
Module Type Foo.
Variable t : Type.
Variable mkFoo : nat -> t.
End Foo.
Module NatFoo : Foo.
Inductive natfoo : Type :=
| mkFoo : nat -> natfoo.
Definition t := natfoo.
End NatFoo.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment