@mathink

フォロー中のタグ18
フォロー中のユーザー3
が、Coqのように暗黙的な変換をcoercionと呼ぶケースは多くないと認識しています。 やはりそうなのですね。 Coq での挙動は強制というには弱いので(強くするわけにはいきませんが)、 どうし…