On Inference and mutually recursive values.

[mariari]

In Minijuvix to express mutually recursive functions one puts their signature before the body

odd? : Nat -> Bool
even? : Nat -> Bool

odd? (S n) = not (even? n)
odd? Z     = false

even? (S n) = not (odd? n)
even? Z     = true

This however will have issues when one has general inference. Ideally minijuvix can tell you the signature of these two functions. Given that HM inference is had.

Thus it would be good to be able to write

odd? (S n) = not (even? n)
odd? Z     = false

even? (S n) = not (odd? n)
even? Z     = true

and have minijuvix tell you the types. This however requires a syntax change.

[jonaprieto]

Look at the issue https://github.com/anoma/juvix/issues/274. We are planning to work on that soon.
If you don't want to write the type signature, you can use an underscore to let the inference do the job for you.