Library CastMonad
The
Cast
monad
Datatype
Transport maps
Monadic operations
Extraction
Example
Decidable instances
Preorder instance
Library DIPop
Pop from list
Type equivalence
Monadic Liftings
Library DIStack
Dependent Stack/Instr
Plain
stack
&
instr
Equivalences
Lifting
Extraction
Library Decidable
The Decidable Class
Decidability
Checkability
A few instances
Reflecting a boolean as a decidable property
Instances for bool
Instances for nat
Instances for list
Instance for decidable equality on list
Instance for less than
Instances for option
Instances for logical connectives
Decidability of proven properties
Library DepEquiv
Dependent equivalences
Properties
Casts for non-dependent functions
Casts from dependent to simple
Library Equiv
Equivalences (first-order)
Functor
class
Type equivalence
Partial Equivalences
Partial Kleisli Equivalences
Injective functions (model constructors)
Instances of IsInjective
Library HODepEquiv
Higher-order dependent equivalences
Domain transformation:
Domain & co-domain transformation:
Argument reordering:
Arity 2 types:
Library HoTT
Library PreOrder
Pointed preorder
Library Showable
The
Show
class
Default Instance:
Instance for nat
Instance for list
Instance for vector
Library Vector
Here are special non dependent useful instantiation of induction
vector <=> list functions
This page has been generated by
coqdoc