Scala example of Exercise 3 from CM 500 Logical Frameworks (see https://github.com/julianpeeters/hello-twelf/tree/main)

even_or_odd.scala

sealed trait Nat
case object Zero extends Nat
case class Successor[A <: Nat](a: A) extends Nat

sealed trait Odd[+N]
case class OddS[N <: Nat](even: Even2[N]) extends Odd[Successor[N]]

sealed trait Even2[+N]
case object Even2Z extends Even2[Zero.type]
case class Even2S[N <: Nat](odd: Odd[N]) extends Even2[Successor[N]]

/* even-or-odd : nat -> type.
 * eo/e : even2 N -> even-or-odd N.
 * eo/o : odd N -> even-or-odd N.
 */
sealed trait EvenOrOdd[+N]
case class EOE[N <: Nat](even2: Even2[N]) extends EvenOrOdd[N]
case class EOO[N <: Nat](odd: Odd[N]) extends EvenOrOdd[N]

/* eo-succ : even-or-odd N -> even-or-odd (s N) -> type.
 * eo-succ/e : eo-succ
 *   (eo/e Even) (eo/o (odd/s Even)).
 * eo-succ/o : eo-succ
 *   (eo/o Odd) (eo/e (even2/s Odd)).
 */
def eoSucc(eon: EvenOrOdd[Nat]): EvenOrOdd[Successor[Nat]] =
  eon match
    case EOE(even2) => EOO(OddS(even2))
    case EOO(odd) => EOE(Even2S(odd))

println("\nEven Or Odd:\n")
println(eoSucc(EOE(Even2Z)))               // EOO(OddS(Even2Z))
println(eoSucc(EOE(Even2S(OddS(Even2Z))))) // EOO(OddS(Even2S(OddS(Even2Z))))
println(eoSucc(EOO(OddS(Even2Z))))         // EOE(Even2S(OddS(Even2Z)))


// every-nat-eo : {N:nat} even-or-odd N -> type.
def everyNatEO(nat: Nat): EvenOrOdd[Nat] =
  nat match
    case Zero => EOE(Even2Z)
    case Successor(n) => eoSucc(everyNatEO(n))

println("\nEvery Nat:\n")
println(everyNatEO(Zero))
println(everyNatEO(Successor(Zero)))
println(everyNatEO(Successor(Successor(Zero))))