How to exhaust the match with in coq using something like default or or clause?

Question

How can i write a switch state similar to this one (in rust), in coq? In particular I'm curios how to merge branches in coq to produce same output, and exhaust the remaining branches via some default implementation.

type Voltages = u32; // in coq is similar to Definition Voltages := R.
type Timestamp = u32; // in coq is similar to Definition Timestamp := R.

const TD: Timestamp = 2; // dummy value cuz rust, in coq would be Variable TD : Timestamp.

enum Pin {
    Ground(bool),
    VoltageIn(bool),
    Threshold,
    Discharge,
    Output,
    Trigger,
    Reset,
    CtrlVoltage
}

impl Pin {
    fn evaluate() -> bool { // dummy for some other functions and predicates
        true
    }
}

fn is_high(p: Pin) -> bool {
    match p {
        Pin::Ground(value) | Pin::VoltageIn(value) => value, // how to grab 2 options in one match in coq?
        _ => Pin.evaluate() // how to exhaust the options in coq?
    }
}

Answer 1

In coq you can separate several branches that bind the same variables by a pipe and use only one right-hand side value. You can also use the underscore as a wildcard to catch all remaining cases.

Inductive t :=
| A (x : nat)
| B (x : nat) (y : bool)
| C (x : unit).

Definition foo (c : t) :=
  match c with
  | A x | B x _ => x
  | _ => 0
  end.