Is such a thing possible to write, or is it preferable to do a different thing to achieve the same result?
By the law of excluded middle for the type $A$ is $A \oplus (A \to Void)$
Here, I meant the
0 type , so should have said
Sorry,
$$lem(A)= A \oplus (A \to \mathbb{0})
$$lem(A)= A \oplus (A \to \mathbb{0})
This can be proved, i.e., we get a term
I am having some trouble in using the replace function.
I was trying to substitute $ 0 $ using the equality in to hopefully get .
But in the function call below:
replace (sym (multZeroRightZero b)) (sym (plusZeroLeftNeutral c))
I am getting an error claiming that in the second variable of replace, idris expects a value of the type P 0. The documentation on this P function couldn't explain much. Any help here would be appreciated.
Is it possible to case split on a dependent pair?
For example, if I want to use the pair
For example, if I want to use the pair
(x **pf) in a function, where I want to case split on x being Z or (S k), and I need the proof when this happens.case (fst (x**pf)) of typechecks, but the proof type does not change, and stays the same as the original.
To capture the notion of a total order, in which exactly one of three things can occur, a<=b and !(a>=b), !(a<=b) and (a>=b) or (a<=b) and (a>=b), would the best thing to do be to define a new type along the lines of Either, or would it be better to try to work with existing types to get something with the same behaviour?
Using combinations of pairs, dependent pairs and coproducts (Either) makes stuff hard to understand, parse by idris and also more error-prone (a wrong type may be accepted because of the same structure).
you can use both definitions
fundamental theorem of arithmetic remains to be done