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)

C (definition)

callrFree [in SSProve.Crypt.rhl_semantics.free_monad.FreeProbProg]
catch [in SSProve.Mon.MonadExamples]
CCA_EVAL_HYB_pkg [in SSProve.Crypt.examples.MACCCA]
CCA_EVAL_HYB_locs [in SSProve.Crypt.examples.MACCCA]
CCA_EVAL_TAG_pkg_ff [in SSProve.Crypt.examples.MACCCA]
CCA_EVAL_TAG_pkg_tt [in SSProve.Crypt.examples.MACCCA]
CCA_EVAL_TAG_locs [in SSProve.Crypt.examples.MACCCA]
CCA_EVAL [in SSProve.Crypt.examples.MACCCA]
CCA_EVAL_pkg_ff [in SSProve.Crypt.examples.MACCCA]
CCA_EVAL_pkg_tt [in SSProve.Crypt.examples.MACCCA]
CCA_EVAL_locs [in SSProve.Crypt.examples.MACCCA]
ceqT_eqType [in SSProve.Crypt.jasmin_util]
cfinT_finType [in SSProve.Crypt.jasmin_util]
chCanonical [in SSProve.Crypt.choice_type]
chCipher [in SSProve.Crypt.examples.KEMDEM]
chDiscr [in SSProve.Crypt.rhl_semantics.only_prob.SubDistr]
checktag [in SSProve.Crypt.examples.MACCCA]
checktag [in SSProve.Crypt.examples.PRFMAC]
check_size_128_256 [in SSProve.Crypt.jasmin_wsize]
check_size_32_64 [in SSProve.Crypt.jasmin_wsize]
check_size_16_64 [in SSProve.Crypt.jasmin_wsize]
check_size_16_32 [in SSProve.Crypt.jasmin_wsize]
check_size_8_32 [in SSProve.Crypt.jasmin_wsize]
check_size_8_64 [in SSProve.Crypt.jasmin_wsize]
check_scale [in SSProve.Crypt.jasmin_word]
chEKey [in SSProve.Crypt.examples.KEMDEM]
chElement [in SSProve.Crypt.choice_type]
chElement_ordType [in SSProve.Crypt.choice_type]
ChiKleisli [in SSProve.Crypt.rhl_semantics.more_categories.OrderEnrichedRelativeAdjunctions]
ChiKleisli0 [in SSProve.Crypt.rhl_semantics.more_categories.OrderEnrichedRelativeAdjunctions]
Chi_CodomainStateAdj [in SSProve.Crypt.rhl_semantics.state_prob.OrderEnrichedRelativeAdjunctionsExamples]
Chi_CodomainStateAdj0 [in SSProve.Crypt.rhl_semantics.state_prob.OrderEnrichedRelativeAdjunctionsExamples]
Chi_DomainStateAdj [in SSProve.Crypt.rhl_semantics.state_prob.OrderEnrichedRelativeAdjunctionsExamples]
Chi_transformedAdjunction [in SSProve.Crypt.rhl_semantics.more_categories.OrderEnrichedRelativeAdjunctions]
chKey [in SSProve.Crypt.examples.KEMDEM]
choice_snd_proj [in SSProve.Crypt.rhl_semantics.ChoiceAsOrd]
choice_fst_proj [in SSProve.Crypt.rhl_semantics.ChoiceAsOrd]
choice_incl [in SSProve.Crypt.rhl_semantics.ChoiceAsOrd]
choice_type_sind [in SSProve.Crypt.choice_type]
choice_type_rec [in SSProve.Crypt.choice_type]
choice_type_ind [in SSProve.Crypt.choice_type]
choice_type_rect [in SSProve.Crypt.choice_type]
choice_Countable__to__choice_Choice_isCountable [in SSProve.Crypt.examples.concrete_groups]
choice_Choice__to__choice_hasChoice [in SSProve.Crypt.examples.concrete_groups]
choice_Choice__to__eqtype_hasDecEq [in SSProve.Crypt.Casts]
choice_Choice__to__choice_hasChoice [in SSProve.Crypt.Casts]
choose [in SSProve.Mon.MonadExamples]
choose_heap [in SSProve.Crypt.package.pkg_invariants]
chSeq [in SSProve.Crypt.examples.SecretSharing]
chSeq [in SSProve.Crypt.examples.SymmRatchet]
chSeq [in SSProve.Crypt.examples.ShamirSecretSharing]
chSet [in SSProve.Crypt.examples.MACCCA]
chSet [in SSProve.Crypt.examples.SecretSharing]
chSet [in SSProve.Crypt.examples.ShamirSecretSharing]
chSet [in SSProve.Crypt.examples.PRFMAC]
chSet [in SSProve.Crypt.examples.PRPCCA]
chsrc [in SSProve.Crypt.package.pkg_core_definition]
chtgt [in SSProve.Crypt.package.pkg_core_definition]
ch_nat [in SSProve.Crypt.package.pkg_interpreter]
ch_nat [in SSProve.Crypt.examples.Executor]
ch2key [in SSProve.Crypt.examples.OTP]
ch2prod [in SSProve.Crypt.package.pkg_distr]
ch2prod_prod2ch [in SSProve.Crypt.package.pkg_distr]
ch2words [in SSProve.Crypt.examples.OTP]
Ciph [in SSProve.Crypt.examples.PRPCCA]
cipher_location [in SSProve.Crypt.examples.PRF]
ciph_to_pair [in SSProve.Crypt.examples.PRPCCA]
Ciph_N [in SSProve.Crypt.examples.PRPCCA]
cmd_bind [in SSProve.Crypt.package.pkg_core_definition]
CMprod [in SSProve.Crypt.rhl_semantics.more_categories.RelativeMonadMorph_prod]
cmp_max [in SSProve.Crypt.jasmin_util]
cmp_min [in SSProve.Crypt.jasmin_util]
cmp_le [in SSProve.Crypt.jasmin_util]
cmp_lt [in SSProve.Crypt.jasmin_util]
cmtSqu [in SSProve.Crypt.rhl_semantics.more_categories.RelativeMonadMorph_prod]
cmtSqu_prod [in SSProve.Crypt.rhl_semantics.more_categories.RelativeMonadMorph_prod]
code_link [in SSProve.Crypt.package.pkg_composition]
cod_rel [in SSProve.Mon.SpecificationMonads]
coerce [in SSProve.Crypt.choice_type]
coerce_kleisli [in SSProve.Crypt.package.pkg_composition]
command_sind [in SSProve.Crypt.package.pkg_core_definition]
command_rec [in SSProve.Crypt.package.pkg_core_definition]
command_ind [in SSProve.Crypt.package.pkg_core_definition]
command_rect [in SSProve.Crypt.package.pkg_core_definition]
commute [in SSProve.Relational.Commutativity]
commute_effObs [in SSProve.Relational.Commutativity]
commuting_unary_base_square [in SSProve.Crypt.rhl_semantics.only_prob.Theta_dens]
comparison_eq_dec [in SSProve.Crypt.jasmin_util]
compl [in SSProve.Crypt.examples.PRPCCA]
compPair [in SSProve.Relational.OrderEnrichedRelativeMonadExamples]
compPairRMonad [in SSProve.Relational.OrderEnrichedRelativeMonadExamples]
compRel [in SSProve.Relational.Rel]
comp_monmon [in SSProve.Mon.SPropMonadicStructures]
comp_monad_morphism [in SSProve.Mon.SPropMonadicStructures]
ComRing_sort__canonical__CountRing_ComRing [in SSProve.Crypt.Casts]
ComRing_sort__canonical__GRing_ComRing [in SSProve.Crypt.Casts]
ComRing_sort__canonical__choice_SubCountable [in SSProve.Crypt.Casts]
ComRing_sort__canonical__Ord_Ord [in SSProve.Crypt.Casts]
concrete_groups_Z3__canonical__fingroup_FinGroup [in SSProve.Crypt.examples.concrete_groups]
concrete_groups_Z3__canonical__fingroup_BaseFinGroup [in SSProve.Crypt.examples.concrete_groups]
concrete_groups_Z3__canonical__fintype_Finite [in SSProve.Crypt.examples.concrete_groups]
concrete_groups_Z3__canonical__choice_Countable [in SSProve.Crypt.examples.concrete_groups]
concrete_groups_Z3__canonical__choice_Choice [in SSProve.Crypt.examples.concrete_groups]
concrete_groups_Z3__canonical__eqtype_Equality [in SSProve.Crypt.examples.concrete_groups]
conc_map [in SSProve.Crypt.jasmin_util]
ConsCtx [in SSProve.Relational.Rel]
cont_perform [in SSProve.Mon.DijkstraMonadExamples]
count_loc [in SSProve.Crypt.examples.PRFPRG]
couple_rhs [in SSProve.Crypt.package.pkg_invariants]
couple_lhs [in SSProve.Crypt.package.pkg_invariants]
coupling [in SSProve.Crypt.rhl_semantics.only_prob.Couplings]
coupling_self_SDistr [in SSProve.Crypt.rules.RulesStateProb]
cpa_epsilon [in SSProve.Crypt.examples.MACCCA]
CPA_EVAL [in SSProve.Crypt.examples.MACCCA]
CPA_EVAL_pkg_ff [in SSProve.Crypt.examples.MACCCA]
CPA_EVAL_pkg_tt [in SSProve.Crypt.examples.MACCCA]
CPA_EVAL_locs [in SSProve.Crypt.examples.MACCCA]
cpa_epsilon [in SSProve.Crypt.examples.SymmRatchet]
Cprod [in SSProve.Crypt.rhl_semantics.more_categories.RelativeMonadMorph_prod]
ctrans [in SSProve.Crypt.jasmin_util]
CTXT [in SSProve.Crypt.examples.SymmRatchet]
ctxt [in SSProve.Crypt.examples.SymmRatchet]
CTXT [in SSProve.Crypt.examples.PRPCCA]
ctxt [in SSProve.Crypt.examples.PRPCCA]
CTXT_pkg_ff [in SSProve.Crypt.examples.SymmRatchet]
CTXT_pkg_tt [in SSProve.Crypt.examples.SymmRatchet]
CTXT_EVAL_pkg_ff [in SSProve.Crypt.examples.PRPCCA]
CTXT_HYB_pkg_5 [in SSProve.Crypt.examples.PRPCCA]
CTXT_HYB_pkg_4 [in SSProve.Crypt.examples.PRPCCA]
CTXT_HYB_pkg_3 [in SSProve.Crypt.examples.PRPCCA]
CTXT_HYB_pkg_2 [in SSProve.Crypt.examples.PRPCCA]
CTXT_HYB_locs_2 [in SSProve.Crypt.examples.PRPCCA]
CTXT_HYB_pkg_1 [in SSProve.Crypt.examples.PRPCCA]
CTXT_HYB_locs_1 [in SSProve.Crypt.examples.PRPCCA]
CTXT_EVAL_SAMP_pkg [in SSProve.Crypt.examples.PRPCCA]
CTXT_EVAL_SAMP_locs [in SSProve.Crypt.examples.PRPCCA]
CTXT_EVAL_pkg_tt [in SSProve.Crypt.examples.PRPCCA]
CTXT_EVAL_locs [in SSProve.Crypt.examples.PRPCCA]
CTXT_pkg_ff [in SSProve.Crypt.examples.PRPCCA]
CTXT_pkg_tt [in SSProve.Crypt.examples.PRPCCA]
CTXT_locs [in SSProve.Crypt.examples.PRPCCA]
cucumber [in SSProve.Crypt.choice_type]
cucumber' [in SSProve.Crypt.choice_type]
CWprod [in SSProve.Crypt.rhl_semantics.more_categories.RelativeMonadMorph_prod]
c_loc [in SSProve.Crypt.examples.KEMDEM]
c_sample [in SSProve.Crypt.rules.RulesStateProb]

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)