Project Page
Index
Table of Contents
OpSemProofs.ennr
Equality
ennr
is a semiring
Misc definitions and facts about
ennr
.
OpSemProofs.utils
Additions to
option
OpSemProofs.entropy
OpSemProofs.integration
Definitions
Axioms of integration
Consequences of the axioms
Measure combinators
Lemmas about integrals
Measures that may be safely interchanged
Other lemmas
OpSemProofs.syntax
Types
Expressions
Values
Using
sig
to program by tactics
Substitution
Evaluation
OpSemProofs.determinism
OpSemProofs.relations
The value measure
μ_e
The logical relation
Tactics
Lemmas
Compatibility Lemmas
The fundamental property
OpSemProofs.chain
OpSemProofs.ctxequiv
Contexts
The
Plug
typeclass
OpSemProofs.properties_of_relations
Symmetry
Transitivity
Reflexivity
Proving expressions are related
OpSemProofs.applications