So I am trying to create something similar to this in Coq:
let rec isval t = match t with | TmTrue(_) -> true | TmFalse(_) -> true | t when isnumericval t -> true | _ -> false
I find the when keyword very convenient to avoid nested if in the match statement. I confirmed that Coq doesn't have this exact keyword, so the question is what is the closest alternative ?.
Of course, you can at least nest an if inside the pattern match. That's also the best AFAICT. Sometimes that requires duplicating the branch body, but you can often let-bind it... (example coming)
suppose instead of
| _ -> false you have a
large_expression as fallback. Using nested if directly duplicates
match t with | TmTrue(_) => true | TmFalse(_) => true | t => if isnumericval t then true else large_expression | _ => large_expression end.
But you can write sth like this:
let fallback := large_expression in match t with | TmTrue(_) => true | TmFalse(_) => true | t => if isnumericval t then true else fallback | _ => fallback end.
Last updated: Oct 04 2023 at 20:01 UTC