Scalaで等価証明を実装することは可能ですか？ Idrisによるタイプドリブン開発では、平等プルーフタイプの定義方法の例を示しています。 data (=): a -> b -> Type where
Refl : x = x
スカラ座にこれを変換するために私の最初の本能は、このようなものです。 sealed trait EqualityProof[A, B]
final case
帰納的データ型の構文を使用しようとしましたが、エラーメッセージがあります。「相互誘導型は従属型除外型の基本誘導型にコンパイルする必要があります」相互再帰関数を定義するための構文は何ですか：以下 はまた、自然数 mutual inductive even, odd
with even: ℕ → Prop
| z: even 0
| n: ∀ n, odd n → even (n + 1)
w
に平等の証明で部分式を置き換えます。 plusDouble : (a:Nat) -> (a + a) = a*2
plusDouble a =
rewrite multCommutative a 2 in
rewrite plusZeroRightNeutral a in Refl
は、だから私は、私は信じているbasicall： lemma1 : {x:Nat} ->