アガダには、Haskellのderiving Eq
節に似たものがあれば、私は以下の関連する質問もあります。例えばアガダのHaskell導出機構
、私はおもちゃ-言語の種類があると、
data Type : Set where
Nat : Type
Prp : Type
それから私は、パターンマッチングとC-c C-a
により決定可能平等を実現することができ、
_≟ₜ_ : Decidable {A = Type} _≡_
Nat ≟ₜ Nat = yes refl
Nat ≟ₜ Prp = no (λ())
Prp ≟ₜ Nat = no (λ())
Prp ≟ₜ Prp = yes refl
これができれば、私は好奇心が強いです何とかHaskellで行われているやり方と同じように機械化または自動化することができます:
data Type = Nat | Prp deriving Eq
ありがとう!
私たちはタイプについて話していますが、Agdaタイプの正式なタイプを実現したいと思います.Natは自然数で、Prpは小さな命題です。
⟦_⟧Type : Type → Set ?
⟦ Nat ⟧Type = ℕ
⟦ Prp ⟧Type = Set
悲しいことに、これはうまくいきません。私は持ち上げてこれを修正しようとしましたが、私はレベル持ち上げを使う方法の手がかりがないので失敗しました。どんな助けもありがとう!私をhumouringため
上記の関数の使用例は次のようになり、
record InterpretedFunctionSymbol : Set where
field
arity : ℕ
src tgt : Type
reify : Vec ⟦ src ⟧Type arity → ⟦ tgt ⟧Type
お礼を!
ありがとうございます。引用論文を読んで、^ _^ –