Skip to content

Instantly share code, notes, and snippets.

@Lysxia

Lysxia/bla.v

Created May 14, 2018 13:08
Show Gist options
  • Save Lysxia/d577b3b3b482b2c41aef3d5ed259caa1 to your computer and use it in GitHub Desktop.
Save Lysxia/d577b3b3b482b2c41aef3d5ed259caa1 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
bla.v
Require Import Nat.
Definition TT (n : nat) : Type := if even n then bool else nat.
Definition bla (n : nat) : TT n.
unfold TT.
destruct (even n).
apply true.
apply 4.
Defined.
Print bla.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment