SSProve.Mon.SpecificationMonads

Global Index

(4242 entries)

Notation Index

B

C

H

I

J

L

N

Q

T

U

V

W

X

Y

Z

_

(243 entries)

Module Index

B

C

H

I

J

K

L

M

N

Q

T

U

V

W

X

Y

_

other

(51 entries)

Variable Index

G

I

J

K

N

Q

V

W

X

Y

Z

_

other

(197 entries)

Library Index

H

N

Q

V

W

X

Y

Z

_

other

(85 entries)

Constructor Index

B

J

K

M

Q

X

Y

other

(122 entries)

Lemma Index

J

Q

_

(1037 entries)

Axiom Index

B

C

F

H

I

J

K

L

M

N

O

P

Q

T

V

W

X

Y

Z

_

other

(66 entries)

Inductive Index

B

G

J

K

M

Q

U

X

Y

_

other

(51 entries)

Projection Index

G

J

Q

T

U

X

Y

Z

other

(271 entries)

Section Index

J

Q

V

X

Y

_

other

(291 entries)

Instance Index

F

H

J

K

N

Q

T

V

X

Y

_

other

(46 entries)

Abbreviation Index

B

C

E

H

J

K

N

Q

T

V

X

Y

_

(68 entries)

Definition Index

X

Y

_

(1638 entries)

Record Index

B

G

H

J

Q

U

W

X

Y

Z

_

other

(76 entries)

R (definition)

r [in SSProve.Crypt.rules.UniformDistrLemmas]
raise [in SSProve.Mon.MonadExamples]
ran [in SSProve.Mon.SPropMonadicStructures]
ran_iso [in SSProve.Mon.SPropMonadicStructures]
ran_mono [in SSProve.Mon.SPropMonadicStructures]
raw_package [in SSProve.Crypt.package.pkg_core_definition]
raw_code_sind [in SSProve.Crypt.package.pkg_core_definition]
raw_code_rec [in SSProve.Crypt.package.pkg_core_definition]
raw_code_ind [in SSProve.Crypt.package.pkg_core_definition]
raw_code_rect [in SSProve.Crypt.package.pkg_core_definition]
read [in SSProve.Mon.MonadExamples]
Rel [in SSProve.Relational.Rel]
RelationalEffectObservation0 [in SSProve.Relational.OrderEnrichedRelativeMonadExamples]
RelationalLaxEffectObservation0 [in SSProve.Relational.OrderEnrichedRelativeMonadExamples]
RelationalSpecMonad0 [in SSProve.Relational.OrderEnrichedRelativeMonadExamples]
relation_from_mmorph [in SSProve.Mon.SPropMonadicStructures]
relativeMonadMorphism_to_lax [in SSProve.Relational.OrderEnrichedCategory]
relativeMonad_postcomposition [in SSProve.Relational.OrderEnrichedCategory]
relativeMonad_precomposition_lax_morph [in SSProve.Relational.OrderEnrichedCategory]
relativeMonad_precomposition_morph [in SSProve.Relational.OrderEnrichedCategory]
relativeMonad_precomposition [in SSProve.Relational.OrderEnrichedCategory]
relativeMonad_postcomposition [in SSProve.Relational.RelativeMonads]
relativeMonad_precomposition_morph [in SSProve.Relational.RelativeMonads]
relativeMonad_precomposition [in SSProve.Relational.RelativeMonads]
RelCat [in SSProve.Relational.Rel]
relKleisli [in SSProve.Crypt.rhl_semantics.more_categories.OrderEnrichedRelativeAdjunctions]
relMon_fromLeftAdj [in SSProve.Crypt.rhl_semantics.more_categories.OrderEnrichedRelativeAdjunctions]
Relw [in SSProve.Relational.Rel]
rel_prod_fmap [in SSProve.Relational.Rel]
rel_prod [in SSProve.Relational.Rel]
rel_one [in SSProve.Relational.Rel]
rel_jdg_sind [in SSProve.Crypt.package.pkg_rhl]
rel_jdg_rec [in SSProve.Crypt.package.pkg_rhl]
rel_jdg_ind [in SSProve.Crypt.package.pkg_rhl]
rel_jdg_rect [in SSProve.Crypt.package.pkg_rhl]
remember_pre [in SSProve.Crypt.package.pkg_invariants]
rem_rhs [in SSProve.Crypt.package.pkg_invariants]
rem_lhs [in SSProve.Crypt.package.pkg_invariants]
repr [in SSProve.Crypt.package.pkg_semantics]
repr_cmd [in SSProve.Crypt.package.pkg_semantics]
resolve [in SSProve.Crypt.package.pkg_composition]
results_from_the_paper [in SSProve.Crypt.Main]
Result.apply [in SSProve.Crypt.jasmin_util]
Result.bind [in SSProve.Crypt.jasmin_util]
Result.default [in SSProve.Crypt.jasmin_util]
Result.map [in SSProve.Crypt.jasmin_util]
ret [in SSProve.Mon.SPropMonadicStructures]
retF [in SSProve.Crypt.rules.RulesStateProb]
retW [in SSProve.Crypt.rules.RulesStateProb]
retW [in SSProve.Relational.OrderEnrichedRelativeMonadExamples]
retWUpd [in SSProve.Mon.SpecificationMonads]
ret_mmorph [in SSProve.Mon.MonadExamples]
rFree [in SSProve.Crypt.rhl_semantics.free_monad.FreeProbProg]
rFreeF_sind [in SSProve.Crypt.rhl_semantics.free_monad.FreeProbProg]
rFreeF_rec [in SSProve.Crypt.rhl_semantics.free_monad.FreeProbProg]
rFreeF_ind [in SSProve.Crypt.rhl_semantics.free_monad.FreeProbProg]
rFreeF_rect [in SSProve.Crypt.rhl_semantics.free_monad.FreeProbProg]
rFreePr [in SSProve.Crypt.rhl_semantics.free_monad.FreeProbProg]
rFreeProb_squ [in SSProve.Crypt.rhl_semantics.free_monad.FreeProbProg]
rFreeProb_squ_fromProd [in SSProve.Crypt.rhl_semantics.free_monad.FreeProbProg]
rightHom [in SSProve.Crypt.rhl_semantics.more_categories.OrderEnrichedRelativeAdjunctions]
rightModule_postcomp [in SSProve.Relational.RelativeMonads]
right_assoc_rlmm_comp [in SSProve.Crypt.rhl_semantics.more_categories.LaxComp]
right_proj_functor [in SSProve.Relational.OrderEnrichedCategory]
right_module_nattrans [in SSProve.Relational.RelativeMonads]
right_proj_functor [in SSProve.Relational.Category]
rlmm_comp [in SSProve.Crypt.rhl_semantics.more_categories.LaxComp]
rlmm_from_lmla [in SSProve.Crypt.rhl_semantics.more_categories.TransformingLaxMorph]
rlmm_codomain [in SSProve.Crypt.rhl_semantics.state_prob.StateTransformingLaxMorph]
rlmm_domain [in SSProve.Crypt.rhl_semantics.state_prob.StateTransformingLaxMorph]
rlmm_codomain [in SSProve.Crypt.rhl_semantics.state_prob.StateTransfThetaDens]
rlmm_domain [in SSProve.Crypt.rhl_semantics.state_prob.StateTransfThetaDens]
rmg [in SSProve.Crypt.rhl_semantics.only_prob.Couplings]
rMonad [in SSProve.Relational.OrderEnrichedRelativeMonadExamples]
rmon_transp_natIso [in SSProve.Relational.OrderEnrichedCategory]
rmon_to_ord_functor [in SSProve.Relational.OrderEnrichedCategory]
rmon_morph_right_module [in SSProve.Relational.RelativeMonads]
rmon_transp_natIso [in SSProve.Relational.RelativeMonads]
rmon_id_mult [in SSProve.Relational.RelativeMonads]
rmon_unit [in SSProve.Relational.RelativeMonads]
rmon_to_functor [in SSProve.Relational.RelativeMonads]
RO.chQuery [in SSProve.Crypt.examples.RandomOracle]
RO.chRandom [in SSProve.Crypt.examples.RandomOracle]
RO.INIT [in SSProve.Crypt.examples.RandomOracle]
RO.i_random [in SSProve.Crypt.examples.RandomOracle]
RO.queries_loc [in SSProve.Crypt.examples.RandomOracle]
RO.QUERY [in SSProve.Crypt.examples.RandomOracle]
RO.RO [in SSProve.Crypt.examples.RandomOracle]
RO.RO_exports [in SSProve.Crypt.examples.RandomOracle]
RO.RO_locs [in SSProve.Crypt.examples.RandomOracle]
RUN [in SSProve.Crypt.package.pkg_advantage]
Run [in SSProve.Crypt.package.pkg_interpreter]
Run [in SSProve.Crypt.examples.Executor]
Run_aux [in SSProve.Crypt.package.pkg_interpreter]
Run_aux [in SSProve.Crypt.examples.Executor]
R_loc [in SSProve.Crypt.examples.PRPCCA]

Global Index

(4242 entries)

Notation Index

B

C

H

I

J

L

N

Q

T

U

V

W

X

Y

Z

_

(243 entries)

Module Index

B

C

H

I

J

K

L

M

N

Q

T

U

V

W

X

Y

_

other

(51 entries)

Variable Index

G

I

J

K

N

Q

V

W

X

Y

Z

_

other

(197 entries)

Library Index

H

N

Q

V

W

X

Y

Z

_

other

(85 entries)

Constructor Index

B

J

K

M

Q

X

Y

other

(122 entries)

Lemma Index

J

Q

_

(1037 entries)

Axiom Index

B

C

F

H

I

J

K

L

M

N

O

P

Q

T

V

W

X

Y

Z

_

other

(66 entries)

Inductive Index

B

G

J

K

M

Q

U

X

Y

_

other

(51 entries)

Projection Index

G

J

Q

T

U

X

Y

Z

other

(271 entries)

Section Index

J

Q

V

X

Y

_

other

(291 entries)

Instance Index

F

H

J

K

N

Q

T

V

X

Y

_

other

(46 entries)

Abbreviation Index

B

C

E

H

J

K

N

Q

T

V

X

Y

_

(68 entries)

Definition Index

X

Y

_

(1638 entries)

Record Index

B

G

H

J

Q

U

W

X

Y

Z

_

other

(76 entries)