agda

2熱

2答えて

遅延コンストラクタなしでCoListを定義しようとしています。私はwith式を使用する問題に遭遇していますが、agdaはサブケースのタイプを洗練しません。 module Failing where open import Data.Unit open import Data.Empty open import Data.Maybe open import Data.Nat open i

1熱

1答えて

AgdaのHaskell型式のメーターが `Raw`で始まっているのはなぜですか？

Agda標準ライブラリでは、我々はRawMonad、RawApplicative、などがあります。.. RawMonad : ∀ {f} → (Set f → Set f) → Set _ RawMonad M = RawIMonad {I = ⊤} (λ _ _ → M) RawMonadZero : ∀ {f} → (Set f → Set f) → Set _ RawMonadZer

0熱

1答えて

`replace`を使ってこの可換性の証拠を完成させるには？

thisのドキュメントには、replaceを使用して証明を完成させる方法が記載されていますが、rewriteが使用されています。これはreplaceという文章砂糖のようです。私はそれを明示的に使用する方法を理解することに興味があります。私が正しく理解していれば、反射性によって証明可能となり、k = plus k 0という証拠与えられ、S (plus k 0) = S (plus k 0)としてS

2熱

3答えて

Agdaの `Vec`に安全な` length`関数を書く方法は？

Data.Vecがあるので、私たちはVecが何であるかを知っています。 NatとVecが同型であることを証明したいと思います。は私はNATがVecをに変換できることを証明機能正常に作成されました： ℕ→vec : (n : ℕ) → Vec ⊤ n ℕ→vec zero = [] ℕ→vec (suc a) = tt ∷ ℕ→vec a 私は、対応するvec→ℕを書くしようとしていたとき

2熱

1答えて

短絡する「面白くない」例

私はこのようなData.Maybe.monadを使用する関数があります。 typeCheck ν (f · e) = typeCheck ν e >>= λ { (u , e′) → typeCheck ν f >>= λ { (u′ ▷ t , f′) → u !≡ₜ u′ >>= λ { refl → pure (, (f′ · e′)) };

1熱

1答えて

Agdaのタイプ解除でエイリアスを定義する方法は？

マイコード： law : ∀ a x → ((suc a) * (suc a) ÷ (suc a) ⟨ x ⟩) →ℕ ≡ (suc a , refl) law a x = refl （このコードはちょうど私の考えを説明し、それがコンパイルされません）私はあまりにも多くのsuc aがあると思うと、私は、suc aにのようなものを別名を与えたい： law : ∀ a x → ((s : suc

2熱

1答えて

Agdaで数えることができる部分集合

私は、ある述語Pによって定義された特定の部分集合に対して数える性質を表現する必要があります。私の最初のアイデアは、私の部分集合の間に全容である関数fが存在することを明示することでした。自然数。標準ライブラリでそのプロパティを表現するもう一つのより一般的な方法がありますか？あなたはあなただけの自然数を使用していない理由を自然数と同型であるセットを使用している場合は事前

2熱

1答えて

実際に等式推論演算子はどのように使用されていますか？

Agda Standard Libraryは、紙に書いたことと同様の方法で証明書を書くことができる演算子や、Haskellコミュニティでどのように教えられているかを書き出す演算子をエクスポートします。あなたはwith抽象化、rewriteまたはヘルパー補助を使用して目標を洗練することによって、「慣習的な」Agdaプルーフを幾分体系的なやり方で書くことができますが、等価推論プリミティブを使った証明が