🅱️ Dependent_bool.v

Translated OCaml

Gitlab , OCaml

File generated by coq-of-ocaml

Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.

Inductive no : Set :=
| DNo : no.

Inductive yes : Set :=
| DYes : yes.

Inductive dbool : Set :=
| No : dbool
| Yes : dbool.

Inductive dand : Set :=
| NoNo : dand
| NoYes : dand
| YesNo : dand
| YesYes : dand.

Inductive ex_dand : Set :=
| Ex_dand : dand → ex_dand.

Definition dand_value (a_value : dbool) (b_value : dbool) : ex_dand :=
  match (a_value, b_value) with
  | (No, No) ⇒ Ex_dand NoNo
  | (No, Yes) ⇒ Ex_dand NoYes
  | (Yes, No) ⇒ Ex_dand YesNo
  | (Yes, Yes) ⇒ Ex_dand YesYes
  end.

Definition dbool_of_dand (function_parameter : dand) : dbool :=
  match function_parameter with
  | NoNo ⇒ No
  | NoYes ⇒ No
  | YesNo ⇒ No
  | YesYes ⇒ Yes
  end.

Inductive eq : Set :=
| Eq : eq.

Definition merge_dand (w1 : dand) (w2 : dand) : eq :=
  match (w1, w2) with
  | (NoNo, NoNo) ⇒ Eq
  | (NoYes, NoYes) ⇒ Eq
  | (YesNo, YesNo) ⇒ Eq
  | (YesYes, YesYes) ⇒ Eq
  | _ ⇒ unreachable_gadt_branch
  end.