GADT.v

(* Default settings (from HsToCoq.Coq.Preamble) *)

Generalizable All Variables.

Unset Implicit Arguments.
Set Maximal Implicit Insertion.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Require Coq.Program.Tactics.
Require Coq.Program.Wf.

(* Converted imports: *)

Require GHC.Types.
Import GHC.Types.Notations.

(* Converted type declarations: *)

Inductive O : Type :=.

Inductive C : Type :=.

Inductive Foo a : _GHC.Types.*_ -> _GHC.Types.*_
  := | Bar : O -> Foo a O
  |  Baz : a -> Foo a C.

Inductive MaybeO ex t : Type
  := | JustO : t -> MaybeO O t
  |  NothingO : MaybeO C t.

Arguments Bar {_}.

Arguments Baz {_}.

Arguments JustO {_} {_}.

Arguments NothingO {_} {_}.

(* Converted value declarations: *)

Definition foo {a} : Foo GHC.Types.Bool a -> GHC.Types.Bool :=
  fun arg_0__ => match arg_0__ with | Bar _ => GHC.Types.True | Baz b => b end.

(* External variables:
     GHC.Types.Bool GHC.Types.True GHC.Types.op_zt__
*)