Library Option


Inductive Option (A : Set) : Set :=
  | Some : forall x : A, Option A
  | None : Option A.
Global Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (4 entries)
Constructor Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (2 entries)
Inductive Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (1 entry)
Library Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (1 entry)

Global Index

N

None [constructor, in Option]


O

Option [inductive, in Option]
Option [library]


S

Some [constructor, in Option]



Constructor Index

N

None [in Option]


S

Some [in Option]



Inductive Index

O

Option [in Option]



Library Index

O

Option



Global Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (4 entries)
Constructor Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (2 entries)
Inductive Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (1 entry)
Library Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (1 entry)

This page has been generated by coqdoc