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 `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: Jun 15 2024 at 08:01 UTC