I've the following code (mostly auto-generated by playing with idris-mode in emacs):
module Main
data Parity : Nat -> Type where
even : (n : Nat) -> Parity (n + n)
odd : (n : Nat) -> Parity (S (n + n))
parity : (n : Nat) -> Parity n
parity Z = ?parity_rhs_1
parity (S Z) = ?parity_rhs_3
parity (S (S k)) with (parity k)
parity (S (S (plus n n))) | (even n) = ?(plus_1 n n)_rhs
parity (S (S (S (plus n n)))) | (odd n) = ?(S_2 (plus n n))_rhs
---------- Proofs ----------
Main.parity_rhs_3 = proof
exact (odd 0)
Main.parity_rhs_1 = proof
exact (even 0)
When trying to load the file into the REPL (C-c C-l) I get the following error message:
- + Errors (1)
`-- ./Main.idr line 11 col 3:
error: expected: "{",
function declaration
parity (S (S (plus n n))) | (even n) = ?(plus_1 n n)_rhs
^
I guess I'm doing something wrong, but I can't figure out what.
$ idris --version
0.9.14.1-git:c6574b4
It's not you who did something wrong, but Idris! The thing after a ? needs to be a valid identifier, so if you replace ?(plus_1 n n)_rhs with something like ?plus_1_n_n_rhs it should be fine.
This is a bug in Idris, but not one I've seen before, or one I can easily reproduce - it generates sensible names when I try to build this. If you can post the steps to reproduce to the issue tracker at https://github.com/idris-lang/Idris-dev/issues then I'll look into it!