-- "A Tutorial on [Co-]Inductive Types in Coq" -- 3.4 Case Analysis and Logical Paradoxes の Agda2版です。 -- Strictly Positiveが要請される1つの理由 module Paradox where open import Data.String data False : Set0 where data Nat : Set0 wher…
引用をストックしました
引用するにはまずログインしてください
引用をストックできませんでした。再度お試しください
限定公開記事のため引用できません。