Top

Module Main

Definition

aiueo```coq aiueo: nat ``` - **full path**: `Main.aiueo`

:= 123.
Definition

kakik```coq kakik: bool ``` - **full path**: `Main.kakik`

:= true.
Require Import Bool.
Definition

eqdec```coq eqdec: forall x y : bool, {x = y} + {x <> y} ``` - **full path**: `Main.eqdec`

: forall x y: bool, {x = y} + {x <> y} := bool_dec.

Require Import ZArith.

Definition

hoge

: {y | (y >= 12)%Z}.
  refine (exist _ 12%Z _). now auto with zarith.