coinduction

2熱

1答えて

fooの新しい型を定義すると、foo_rectという再帰の原理が得られます。この再帰の原理は、fixを基にしています。どのようにして「矢印を反転させる」ことによって、コインシデンス相当物（cofixで要約）を定義できますか？

6熱

1答えて

私は、次のセクション4に示すように、並列プリエンプティブスケジューリングを使用してIMP言語の機能セマンティクスをコーディングしようとしています。paper。私はAgda 2.5.2と標準ライブラリ0.13を使用しています。また、コード全体は、gistで利用可能です。まず、問題の言語の構文を誘導型と定義しました。 data Exp (n : ℕ) : Set where $_ : ℕ

2熱

1答えて

Coq on Coinduction、タイプミスマッチ

私はコインシデンスタイプを試していましたし、自然数とベクトル（型のサイズがリスト）のコインシデンスバージョンを定義することに決めました。私は彼らとように無限の数に定義： CoInductive conat : Set := | cozero : conat | cosuc : conat -> conat. CoInductive covec (A : Set) : conat -> Se

1熱

1答えて

共自然数の共導入原理を証明する

私は共導入があまりよくないと認めなければなりません。私は共自然数で二重共鳴の原理を示すことを試みていますが、私は（対称の）対の場合についています。 CoInductive conat := | cozero : conat | cosucc : conat -> conat. CoInductive conat_eq : conat -> conat -> Prop :=