Skip to content

Instantly share code, notes, and snippets.

@yoshihiro503

yoshihiro503/Otoshiana.v

Created August 28, 2015 10:33
Show Gist options
  • Save yoshihiro503/c909dc5186d0898d4c12 to your computer and use it in GitHub Desktop.
Save yoshihiro503/c909dc5186d0898d4c12 to your computer and use it in GitHub Desktop.
Download ZIP
なぞなぞ：Coqの関数定義でなぜか戻り値がSetじゃないとダメと起こられる例:
Raw
Otoshiana.v
Definition foo (b : bool) : nat =
if b then 0 else 1.
@yoshihiro503
Copy link
Author

このCoqコードはエラーとなって次のエラーメッセージが返される(Coq-8.2)

Error: In environment
b : bool
The term "0" has type "nat" while it is expected to have type 
"Set".

それはなぜでしょう？

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment