Stream: Coq users

Topic: Does Coq have equivalent for Ocaml's `match ... when`

walker (Aug 12 2022 at 17:11):

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 ?.

Paolo Giarrusso (Aug 12 2022 at 17:39):

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)

Paolo Giarrusso (Aug 12 2022 at 17:42):

suppose instead of | _ -> false you have a large_expression as fallback. Using nested if directly duplicates large_expression:

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 13 2024 at 01:02 UTC