Lars Hupel

I just realized one could possibly build that on top of the existing primitives. ```scala case class Common(x: Int = 3, y: String = "bla") case class Command[T](@Recurse common: Common,...

Yes, keywords are all lowercase. Sometimes things get all caps identifiers, e.g. in Isabelle/ML code.

We could switch to a lowercase convention in cyp too. I don't feel strongly about it.

What would you expect here?

Good idea; sounds reasonably easy to implement. > Anyway, does cyp have nested induction proofs? Then "IH" would be overloaded as well. This _should_ work (with the outer "IH" being...

Would you mind if I included your tree example in this repository?

"List" here refers to the name of the type constructor, i.e., which induction rule to select. But if we get type checking at some point I'm inclined to allow (or...

Do you want the type signatures to be actually checked? Or do they merely have documentation status?

No. Cyp is completely untyped.

I just found this: [haskell-tc](https://github.com/haskell-suite/haskell-tc). So it could be implemented. But I don't see myself having the time to do it 😦