IfElseExpression.v

Module VersionA.
  Inductive bool : Type :=
  | true : bool
  | false : bool.

  Definition neg (b : bool) : bool :=
    if b then false else true.

  Eval compute in (neg true). (* false *)
End VersionA.

Module VersionB.
  Inductive bool : Type :=
  | false : bool
  | true : bool.

  Definition neg (b : bool) : bool :=
    if b then false else true.

  Eval compute in (neg true). (* true *)
End VersionB.