Следующий код: Idris:
natAssociative : (a : Nat) -> (b : Nat) -> (c : Nat) -> (a + b) + c = a + (b + c)
natAssociative Z b c = the (b + c = b + c) refl
natAssociative (S k) b c = replace {P=\x => S (k + b) + c = S x} (natAssociative k b c) refl
Мне очень тяжело переводить это в бесформенное. Я пробовал несколько разных кодировок, но я думаю, что это был самый многообещающий старт:
import scalaz.Leibniz._
import shapeless.{ HNil, Nat, Succ, Poly3 }
import shapeless.Nat._
import shapeless.ops.nat._
object natAssociative extends Poly3 {
implicit def case0[B <: Nat, C <: Nat]: Case[_0, B, C] = at[_0, B, C] {
case (Nat._0, b, c) => refl[Sum[B, C]#Out]
}
implicit def caseSucc[K <: Nat, B <: Nat, C <: Nat] = ???
}
У меня возникают проблемы с индукцией и принятие Scala признают, что у нас есть 2 возможных случая, чтобы рекурсировать. Есть ли трюк для кодирования этой части?