Skip to content

Instantly share code, notes, and snippets.

@yoshihiro503

yoshihiro503/SigSample.v

Created July 22, 2014 09:49
Show Gist options
  • Save yoshihiro503/5b89193251895c075674 to your computer and use it in GitHub Desktop.
Save yoshihiro503/5b89193251895c075674 to your computer and use it in GitHub Desktop.
Download ZIP
sig_sample
Raw
SigSample.v
Require Import Arith.
Definition x : {n | n > 0}.
Proof.
refine (@exist nat (fun n => n > 0) 10 _).
auto 10.
auto with arith.
Defined.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment