Skip to content

Instantly share code, notes, and snippets.

@xyx-is

xyx-is/Coq_match_strange_error.v

Created March 11, 2013 06:39
Show Gist options
  • Save xyx-is/5132249 to your computer and use it in GitHub Desktop.
Save xyx-is/5132249 to your computer and use it in GitHub Desktop.
Download ZIP
tmpの定義には成功しているのに、なぜか普通のパターンマッチtmp2でエラーが出る ( Coq 8.4 (August 2012) )
Raw
Coq_match_strange_error.v
Inductive vect (a:Set) :forall b:Type, a -> b -> Type:=
| vnilt (x:a) b (y:b) : vect a b x y.
Definition tmp:=vnilt nat 1 bool true.
Check tmp. (* vect nat bool 1 true *)
Definition tmp2:nat :=match tmp with z => 1 end. (* error *)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment