For their `add` example, I imagine just having x<y somewhere is sufficient. But let's say I write a sorting implementation but the compiler can't quite figure out that it is correct. Is there a provided way to tell the compiler 'trust me, this property is now true'?
Also, I'm assuming the compiler has two classes of errors here: a counter example vs. unable to prove?
Can anyone point me to documentation on these (in Idris, preferably)?
If you wanted to prove that a list was sorted, you'd write another datatype:
IsSorted : Ord a => List a -> Type
(l : List a ** IsSorted l)
The compiler doesn't generally come up with counterexamples for you; with this style, if the proof isn't complete, it won't compile.