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)

P

pack [projection, in SSProve.Crypt.package.pkg_core_definition]
package [record, in SSProve.Crypt.package.pkg_core_definition]
Package [library]
PackageNotation [module, in SSProve.Crypt.package.pkg_notation]
PackageNotation.gfin [abbreviation, in SSProve.Crypt.package.pkg_notation]
PackageNotation.give_fin [lemma, in SSProve.Crypt.package.pkg_notation]
interface:#val #[ _ ] : _ → _ [notation, in SSProve.Crypt.package.pkg_notation]
package:#def #[ _ ] ( ' _ : _ ) : _ { _ } (package_scope) [notation, in SSProve.Crypt.package.pkg_notation]
package:#def #[ _ ] ( _ : _ ) : _ { _ } (package_scope) [notation, in SSProve.Crypt.package.pkg_notation]
pack_op:#[ _ ] : _ → _ [notation, in SSProve.Crypt.package.pkg_notation]
pack_type:( _ ) [notation, in SSProve.Crypt.package.pkg_notation]
pack_type:_ ∐ _ [notation, in SSProve.Crypt.package.pkg_notation]
pack_type:_ × _ [notation, in SSProve.Crypt.package.pkg_notation]
pack_type:{map _ → _ } [notation, in SSProve.Crypt.package.pkg_notation]
pack_type:'fin _ [notation, in SSProve.Crypt.package.pkg_notation]
pack_type:'option _ [notation, in SSProve.Crypt.package.pkg_notation]
pack_type:'word _ [notation, in SSProve.Crypt.package.pkg_notation]
pack_type:'unit [notation, in SSProve.Crypt.package.pkg_notation]
pack_type:'bool [notation, in SSProve.Crypt.package.pkg_notation]
pack_type:'int [notation, in SSProve.Crypt.package.pkg_notation]
pack_type:'nat [notation, in SSProve.Crypt.package.pkg_notation]
#import _ as _ ;; _ (package_scope) [notation, in SSProve.Crypt.package.pkg_notation]
_ ;' _ (package_scope) [notation, in SSProve.Crypt.package.pkg_notation]
' _ ← cmd _ ;; _ (package_scope) [notation, in SSProve.Crypt.package.pkg_notation]
_ ← cmd _ ;; _ (package_scope) [notation, in SSProve.Crypt.package.pkg_notation]
_ <$ _ ;; _ (package_scope) [notation, in SSProve.Crypt.package.pkg_notation]
' _ ← sample _ ;; _ (package_scope) [notation, in SSProve.Crypt.package.pkg_notation]
_ ← sample _ ;; _ (package_scope) [notation, in SSProve.Crypt.package.pkg_notation]
' _ ← op _ ⋅ _ ;; _ (package_scope) [notation, in SSProve.Crypt.package.pkg_notation]
_ ← op _ ⋅ _ ;; _ (package_scope) [notation, in SSProve.Crypt.package.pkg_notation]
' _ ← get _ ;; _ (package_scope) [notation, in SSProve.Crypt.package.pkg_notation]
_ ← get _ ;; _ (package_scope) [notation, in SSProve.Crypt.package.pkg_notation]
#put _ := _ ;; _ (package_scope) [notation, in SSProve.Crypt.package.pkg_notation]
_ ;; _ (package_scope) [notation, in SSProve.Crypt.package.pkg_notation]
' _ ← _ ;; _ (package_scope) [notation, in SSProve.Crypt.package.pkg_notation]
_ ← _ ;; _ (package_scope) [notation, in SSProve.Crypt.package.pkg_notation]
{ sig _ } (package_scope) [notation, in SSProve.Crypt.package.pkg_notation]
[ package _ ; _ ; _ ; .. ; _ ] (package_scope) [notation, in SSProve.Crypt.package.pkg_notation]
[ package _ ; _ ] (package_scope) [notation, in SSProve.Crypt.package.pkg_notation]
[ package _ ] (package_scope) [notation, in SSProve.Crypt.package.pkg_notation]
[ interface _ ; _ ; .. ; _ ] (package_scope) [notation, in SSProve.Crypt.package.pkg_notation]
[ interface _ ] (package_scope) [notation, in SSProve.Crypt.package.pkg_notation]
[ interface ] (package_scope) [notation, in SSProve.Crypt.package.pkg_notation]
_ ∐ _ (package_scope) [notation, in SSProve.Crypt.package.pkg_notation]
_ × _ (package_scope) [notation, in SSProve.Crypt.package.pkg_notation]
'fin _ (package_scope) [notation, in SSProve.Crypt.package.pkg_notation]
'option _ (package_scope) [notation, in SSProve.Crypt.package.pkg_notation]
'word _ (package_scope) [notation, in SSProve.Crypt.package.pkg_notation]
'unit (package_scope) [notation, in SSProve.Crypt.package.pkg_notation]
'bool (package_scope) [notation, in SSProve.Crypt.package.pkg_notation]
'int (package_scope) [notation, in SSProve.Crypt.package.pkg_notation]
'nat (package_scope) [notation, in SSProve.Crypt.package.pkg_notation]
package_ext [lemma, in SSProve.Crypt.package.pkg_core_definition]
package_usage_example [library]
pack_valid [projection, in SSProve.Crypt.package.pkg_core_definition]
padv_equiv [definition, in SSProve.Crypt.package.pkg_rhl]
Pairs_of_probabilistic_computations [section, in SSProve.Crypt.rhl_semantics.free_monad.FreeProbProg]
par [definition, in SSProve.Crypt.package.pkg_composition]
PartAlg [definition, in SSProve.Mon.DijkstraMonadExamples]
Partiality [section, in SSProve.Mon.MonadExamples]
Party [definition, in SSProve.Crypt.examples.ShamirSecretSharing]
party_to_word [definition, in SSProve.Crypt.examples.ShamirSecretSharing]
par_assoc [lemma, in SSProve.Crypt.package.pkg_composition]
par_commut [lemma, in SSProve.Crypt.package.pkg_composition]
paste [definition, in SSProve.Crypt.rhl_semantics.more_categories.LaxFunctorsAndTransf]
PastingTwoLaxSquares [section, in SSProve.Crypt.rhl_semantics.more_categories.LaxFunctorsAndTransf]
PastingTwoLaxSquares.KCoR1 [variable, in SSProve.Crypt.rhl_semantics.more_categories.LaxFunctorsAndTransf]
PastingTwoLaxSquares.KCoR1oL1 [variable, in SSProve.Crypt.rhl_semantics.more_categories.LaxFunctorsAndTransf]
PastingTwoLaxSquares.KDoL1 [variable, in SSProve.Crypt.rhl_semantics.more_categories.LaxFunctorsAndTransf]
PastingTwoLaxSquares.lKC [variable, in SSProve.Crypt.rhl_semantics.more_categories.LaxFunctorsAndTransf]
PastingTwoLaxSquares.lKI [variable, in SSProve.Crypt.rhl_semantics.more_categories.LaxFunctorsAndTransf]
PastingTwoLaxSquares.lL1 [variable, in SSProve.Crypt.rhl_semantics.more_categories.LaxFunctorsAndTransf]
PastingTwoLaxSquares.lL2 [variable, in SSProve.Crypt.rhl_semantics.more_categories.LaxFunctorsAndTransf]
PastingTwoLaxSquares.lR1 [variable, in SSProve.Crypt.rhl_semantics.more_categories.LaxFunctorsAndTransf]
PastingTwoLaxSquares.lR2 [variable, in SSProve.Crypt.rhl_semantics.more_categories.LaxFunctorsAndTransf]
PastingTwoLaxSquares.L2oKI [variable, in SSProve.Crypt.rhl_semantics.more_categories.LaxFunctorsAndTransf]
PastingTwoLaxSquares.R2oKD [variable, in SSProve.Crypt.rhl_semantics.more_categories.LaxFunctorsAndTransf]
PastingTwoLaxSquares.R2oKDoL1 [variable, in SSProve.Crypt.rhl_semantics.more_categories.LaxFunctorsAndTransf]
PastingTwoLaxSquares.R2oL2oKI [variable, in SSProve.Crypt.rhl_semantics.more_categories.LaxFunctorsAndTransf]
pdep [definition, in SSProve.Crypt.jasmin_word]
pdisjoint [definition, in SSProve.Crypt.package.pkg_invariants]
pelem [inductive, in SSProve.Crypt.jasmin_wsize]
pempty [definition, in SSProve.Crypt.examples.package_usage_example]
pextr [definition, in SSProve.Crypt.jasmin_word]
PE1 [constructor, in SSProve.Crypt.jasmin_wsize]
PE128 [constructor, in SSProve.Crypt.jasmin_wsize]
PE16 [constructor, in SSProve.Crypt.jasmin_wsize]
PE2 [constructor, in SSProve.Crypt.jasmin_wsize]
PE32 [constructor, in SSProve.Crypt.jasmin_wsize]
PE4 [constructor, in SSProve.Crypt.jasmin_wsize]
PE64 [constructor, in SSProve.Crypt.jasmin_wsize]
PE8 [constructor, in SSProve.Crypt.jasmin_wsize]
pf [projection, in SSProve.Mon.Base]
pheap_ignore_empty [lemma, in SSProve.Crypt.package.pkg_invariants]
pheap_ignore [definition, in SSProve.Crypt.package.pkg_invariants]
phi13 [definition, in SSProve.Crypt.rhl_semantics.more_categories.LaxComp]
pick [definition, in SSProve.Mon.MonadExamples]
pick_set [definition, in SSProve.Mon.MonadExamples]
pify [abbreviation, in SSProve.Crypt.jasmin_util]
pInvariant [record, in SSProve.Crypt.package.pkg_invariants]
pInvariant_pheap_ignore [lemma, in SSProve.Crypt.package.pkg_invariants]
pinv_empty [projection, in SSProve.Crypt.package.pkg_invariants]
pinv_pINV' [projection, in SSProve.Crypt.package.pkg_invariants]
pINV' [definition, in SSProve.Crypt.package.pkg_invariants]
pINV'_pheap_ignore [lemma, in SSProve.Crypt.package.pkg_invariants]
pINV'_to_INV [lemma, in SSProve.Crypt.package.pkg_invariants]
PKDEC [definition, in SSProve.Crypt.examples.KEMDEM]
PKENC [definition, in SSProve.Crypt.examples.KEMDEM]
PkeyPair [definition, in SSProve.Crypt.examples.KEMDEM]
PKE_security [lemma, in SSProve.Crypt.examples.KEMDEM]
PKE_CCA_perf_true [lemma, in SSProve.Crypt.examples.KEMDEM]
PKE_CCA_perf [lemma, in SSProve.Crypt.examples.KEMDEM]
PKE_inv [definition, in SSProve.Crypt.examples.KEMDEM]
PKE_CCA [definition, in SSProve.Crypt.examples.KEMDEM]
PKE_CCA_pkg [definition, in SSProve.Crypt.examples.KEMDEM]
PKE_CCA_out [definition, in SSProve.Crypt.examples.KEMDEM]
PKE_CCA_loc [definition, in SSProve.Crypt.examples.KEMDEM]
PKE_dec [projection, in SSProve.Crypt.examples.KEMDEM]
PKE_enc [projection, in SSProve.Crypt.examples.KEMDEM]
PKE_kgen [projection, in SSProve.Crypt.examples.KEMDEM]
PKE_scheme [record, in SSProve.Crypt.examples.KEMDEM]
PKGEN [definition, in SSProve.Crypt.examples.KEMDEM]
pkg_rhl [library]
pkg_core_definition [library]
pkg_interpreter [library]
pkg_advantage [library]
pkg_heap [library]
pkg_composition [library]
pkg_notation [library]
pkg_user_util [library]
pkg_tactics [library]
pkg_invariants [library]
pkg_distr [library]
pkg_semantics [library]
pk_loc [definition, in SSProve.Crypt.examples.KEMDEM]
plain_location [definition, in SSProve.Crypt.examples.PRF]
plus [definition, in SSProve.Crypt.examples.OTP]
plus [definition, in SSProve.Crypt.examples.SecretSharing]
plus [definition, in SSProve.Crypt.examples.PRF]
plus_assoc [lemma, in SSProve.Crypt.examples.OTP]
plus_comm [lemma, in SSProve.Crypt.examples.OTP]
plus_involutive [lemma, in SSProve.Crypt.examples.OTP]
plus_involutive [lemma, in SSProve.Crypt.examples.SecretSharing]
plus_assoc [lemma, in SSProve.Crypt.examples.SecretSharing]
plus_involutive [lemma, in SSProve.Crypt.examples.PRF]
pmulr_me [lemma, in SSProve.Crypt.package.pkg_rhl]
pnth [definition, in SSProve.Crypt.jasmin_util]
points [definition, in SSProve.Relational.Rel]
pointwiseAction [definition, in SSProve.Mon.Monoid]
pointwiseActionFromLaws [definition, in SSProve.Mon.Monoid]
PointwiseFormula [section, in SSProve.Crypt.rhl_semantics.more_categories.LaxComp]
_ \O _ [notation, in SSProve.Crypt.rhl_semantics.more_categories.LaxComp]
pointwiseMonoid [definition, in SSProve.Mon.Monoid]
pointwise_preorder [instance, in SSProve.Mon.SPropMonadicStructures]
pointwise_action [definition, in SSProve.Mon.Monoid]
pointwise_eq_ext [instance, in SSProve.Crypt.package.pkg_tactics]
point_to_homomorphism_to_point [lemma, in SSProve.Relational.RelativeMonads]
point_to_homomorphism [definition, in SSProve.Relational.RelativeMonads]
PolyEnc [definition, in SSProve.Crypt.examples.ShamirSecretSharing]
PolynomialUtils [library]
poly_nat_poly [lemma, in SSProve.Crypt.examples.ShamirSecretSharing]
poly_to_nat [definition, in SSProve.Crypt.examples.ShamirSecretSharing]
poly_bij [definition, in SSProve.Crypt.examples.ShamirSecretSharing]
popcnt [definition, in SSProve.Crypt.jasmin_word]
pos [projection, in SSProve.Crypt.Prelude]
positive [record, in SSProve.Crypt.Prelude]
Positive [record, in SSProve.Crypt.Prelude]
Positive [inductive, in SSProve.Crypt.Prelude]
PositiveEqDec [instance, in SSProve.Crypt.Prelude]
PositiveExp2 [instance, in SSProve.Crypt.Prelude]
PositiveInFin [definition, in SSProve.Crypt.Prelude]
positiveO [instance, in SSProve.Crypt.jasmin_util]
positive_ext [lemma, in SSProve.Crypt.Prelude]
Positive_Lt [instance, in SSProve.Crypt.Prelude]
positive_eqP [lemma, in SSProve.Crypt.Prelude]
positive_eq [definition, in SSProve.Crypt.Prelude]
Positive_prod [lemma, in SSProve.Crypt.Prelude]
postcond [definition, in SSProve.Crypt.package.pkg_invariants]
posteq_rlmm_proper [lemma, in SSProve.Crypt.rhl_semantics.more_categories.LaxComp]
postLeq_rlmm_proper [lemma, in SSProve.Crypt.rhl_semantics.more_categories.LaxComp]
post_conclusion_rule [lemma, in SSProve.Crypt.rules.RulesStateProb]
post_weaken_rule [lemma, in SSProve.Crypt.rules.RulesStateProb]
post_smBeta'' [definition, in SSProve.Crypt.rhl_semantics.more_categories.TransformingLaxMorph]
post_smAlpha'' [definition, in SSProve.Crypt.rhl_semantics.more_categories.TransformingLaxMorph]
pos_eqP [lemma, in SSProve.Crypt.jasmin_util]
Pos_lt_leb_trans [lemma, in SSProve.Crypt.jasmin_util]
Pos_leb_trans [lemma, in SSProve.Crypt.jasmin_util]
pow2nz [lemma, in SSProve.Crypt.jasmin_word]
pow2pos [lemma, in SSProve.Crypt.jasmin_word]
pow2_inj [lemma, in SSProve.Crypt.examples.SecretSharing]
Pr [definition, in SSProve.Crypt.package.pkg_advantage]
precond [definition, in SSProve.Crypt.package.pkg_invariants]
Pred [section, in SSProve.Mon.SpecificationMonads]
Pred_op_order_prorder [instance, in SSProve.Mon.SPropMonadicStructures]
Pred_op_order [definition, in SSProve.Mon.SPropMonadicStructures]
preeq_rlmm_proper' [lemma, in SSProve.Crypt.rhl_semantics.more_categories.LaxComp]
preeq_rlmm_proper [lemma, in SSProve.Crypt.rhl_semantics.more_categories.LaxComp]
preInterpretState [definition, in SSProve.Crypt.rhl_semantics.state_prob.StateTransformingLaxMorph]
preLeq_rlmm_proper [lemma, in SSProve.Crypt.rhl_semantics.more_categories.LaxComp]
Prelude [library]
Prelude_positive__canonical__eqtype_Equality [definition, in SSProve.Crypt.Prelude]
PreorderInstHom [definition, in SSProve.Crypt.rhl_semantics.more_categories.OrderEnrichedRelativeAdjunctions]
PreorderIso [section, in SSProve.Crypt.rhl_semantics.more_categories.OrderEnrichedRelativeAdjunctions]
PreorderMorph [section, in SSProve.Crypt.rhl_semantics.more_categories.OrderEnrichedRelativeAdjunctions]
PrePost [module, in SSProve.Mon.SpecificationMonads]
PrePostSpec [definition, in SSProve.Mon.SpecificationMonads]
PrePostSpec [section, in SSProve.Mon.SpecificationMonads]
PrePostSpec.Ran [section, in SSProve.Mon.SpecificationMonads]
PrePost.PP [definition, in SSProve.Mon.SpecificationMonads]
PrePost.PPSpecMonad [definition, in SSProve.Mon.SpecificationMonads]
PrePost.PPSpecRan [definition, in SSProve.Mon.SpecificationMonads]
PrePost.PPSpec_ran_universal [lemma, in SSProve.Mon.SpecificationMonads]
PrePost.PPSpec_ran_valid [lemma, in SSProve.Mon.SpecificationMonads]
PrePost.PPSpec_ran [definition, in SSProve.Mon.SpecificationMonads]
PrePost.PP_aa [instance, in SSProve.Mon.SpecificationMonads]
PrePost.PP_rel_preorder [instance, in SSProve.Mon.SpecificationMonads]
PrePost.PP_rel [definition, in SSProve.Mon.SpecificationMonads]
PrePost.PP_monad [definition, in SSProve.Mon.SpecificationMonads]
PrePost.PP_bind [definition, in SSProve.Mon.SpecificationMonads]
PrePost.PP_ret [definition, in SSProve.Mon.SpecificationMonads]
PrePost.RightKanExtension [section, in SSProve.Mon.SpecificationMonads]
preRelationalSpecMonad [definition, in SSProve.Relational.OrderEnrichedRelativeMonadExamples]
preserve_update_triple_rhs_lookup_None [lemma, in SSProve.Crypt.package.pkg_invariants]
preserve_update_couple_rhs_lookup_None [lemma, in SSProve.Crypt.package.pkg_invariants]
preserve_update_couple_lhs_lookup_None [lemma, in SSProve.Crypt.package.pkg_invariants]
preserve_update_triple_rhs_lookup [lemma, in SSProve.Crypt.package.pkg_invariants]
preserve_update_couple_rhs_lookup [lemma, in SSProve.Crypt.package.pkg_invariants]
preserve_update_couple_lhs_lookup [lemma, in SSProve.Crypt.package.pkg_invariants]
preserve_update_filter_triple_rhs [lemma, in SSProve.Crypt.package.pkg_invariants]
preserve_update_filter_couple_rhs [lemma, in SSProve.Crypt.package.pkg_invariants]
preserve_update_filter_couple_lhs [lemma, in SSProve.Crypt.package.pkg_invariants]
preserve_update_r_ignored_heap_ignore [lemma, in SSProve.Crypt.package.pkg_invariants]
preserve_update_l_ignored_heap_ignore [lemma, in SSProve.Crypt.package.pkg_invariants]
preserve_update_cons_sym_heap_ignore [lemma, in SSProve.Crypt.package.pkg_invariants]
preserve_update_cons_sym_eq [lemma, in SSProve.Crypt.package.pkg_invariants]
preserve_update_mem_conj [lemma, in SSProve.Crypt.package.pkg_invariants]
preserve_update_mem_nil [lemma, in SSProve.Crypt.package.pkg_invariants]
preserve_update_pre_mem [lemma, in SSProve.Crypt.package.pkg_invariants]
preserve_update_pre [abbreviation, in SSProve.Crypt.package.pkg_invariants]
preserve_update_mem [definition, in SSProve.Crypt.package.pkg_invariants]
pre_strong_hypothesis_rule [lemma, in SSProve.Crypt.rules.RulesStateProb]
pre_hypothesis_rule [lemma, in SSProve.Crypt.rules.RulesStateProb]
pre_weaken_rule [lemma, in SSProve.Crypt.rules.RulesStateProb]
pre_smBeta'' [definition, in SSProve.Crypt.rhl_semantics.more_categories.TransformingLaxMorph]
pre_smAlpha'' [definition, in SSProve.Crypt.rhl_semantics.more_categories.TransformingLaxMorph]
PRF [library]
'word (package_scope) [notation, in SSProve.Crypt.examples.PRFPRG]
pack_type:'word [notation, in SSProve.Crypt.examples.PRFPRG]
PRFGEN_example.n [variable, in SSProve.Crypt.examples.PRFPRG]
PRFGEN_example [section, in SSProve.Crypt.examples.PRFPRG]
PRFMAC [library]
'word (package_scope) [notation, in SSProve.Crypt.examples.PRFMAC]
pack_type:'word [notation, in SSProve.Crypt.examples.PRFMAC]
PRFMAC_example.n [variable, in SSProve.Crypt.examples.PRFMAC]
PRFMAC_example [section, in SSProve.Crypt.examples.PRFMAC]
PRFPRG [library]
prf_epsilon [definition, in SSProve.Crypt.examples.PRF]
pack_type:'key [notation, in SSProve.Crypt.examples.PRF]
pack_type:'word [notation, in SSProve.Crypt.examples.PRF]
_ ⊕ _ [notation, in SSProve.Crypt.examples.PRF]
PRF_example [section, in SSProve.Crypt.examples.PRF]
prf_epsilon [definition, in SSProve.Crypt.examples.PRFMAC]
prf_epsilon [definition, in SSProve.Crypt.examples.PRFPRG]
prg_epsilon [definition, in SSProve.Crypt.examples.StretchPRG]
prg_epsilon [definition, in SSProve.Crypt.examples.SymmRatchet]
ProbAr [definition, in SSProve.Mon.FiniteProbabilities]
ProbM [definition, in SSProve.Mon.FiniteProbabilities]
probopStP [definition, in SSProve.Crypt.rhl_semantics.state_prob.StateTransformingLaxMorph]
ProbS [definition, in SSProve.Mon.FiniteProbabilities]
Prob_arities [definition, in SSProve.Crypt.package.pkg_core_definition]
Prob_ops_collection [definition, in SSProve.Crypt.package.pkg_core_definition]
prodAction [definition, in SSProve.Mon.Monoid]
prodActionFromLaws [definition, in SSProve.Mon.Monoid]
prodMonoid [definition, in SSProve.Mon.Monoid]
ProductCat [section, in SSProve.Relational.OrderEnrichedCategory]
ProductCat [section, in SSProve.Relational.Category]
ProductFunctor [section, in SSProve.Relational.OrderEnrichedCategory]
ProductFunctor [section, in SSProve.Relational.Category]
ProductRelativeMonad [section, in SSProve.Relational.OrderEnrichedCategory]
ProductRelativeMonad [section, in SSProve.Relational.RelativeMonads]
product_action [definition, in SSProve.Mon.Monoid]
product_rmon [definition, in SSProve.Relational.OrderEnrichedCategory]
product_rmon [definition, in SSProve.Relational.RelativeMonads]
prod_comp_coupling [definition, in SSProve.Crypt.rules.RulesStateProb]
prod_comp [definition, in SSProve.Crypt.rules.RulesStateProb]
prod_rel [definition, in SSProve.Relational.OrderEnrichedRelativeMonadExamples]
prod_uniform [lemma, in SSProve.Crypt.rules.UniformDistrLemmas]
prod_uniform.SD_ret [variable, in SSProve.Crypt.rules.UniformDistrLemmas]
prod_uniform.SD_bind [variable, in SSProve.Crypt.rules.UniformDistrLemmas]
prod_uniform [section, in SSProve.Crypt.rules.UniformDistrLemmas]
Prod_of_choiceTypes [section, in SSProve.Crypt.rhl_semantics.ChoiceAsOrd]
prod_functor [definition, in SSProve.Relational.OrderEnrichedCategory]
prod_cat [definition, in SSProve.Relational.OrderEnrichedCategory]
prod_finType [definition, in SSProve.Crypt.Casts]
prod_choiceType [definition, in SSProve.Crypt.Casts]
prod_relativeMonadMorphism [definition, in SSProve.Crypt.rhl_semantics.more_categories.RelativeMonadMorph_prod]
prod_natIso [definition, in SSProve.Crypt.rhl_semantics.more_categories.RelativeMonadMorph_prod]
prod_functor [definition, in SSProve.Relational.Category]
prod_cat [definition, in SSProve.Relational.Category]
prod2ch [definition, in SSProve.Crypt.package.pkg_distr]
prod2ch_ch2prod [definition, in SSProve.Crypt.package.pkg_distr]
prog [projection, in SSProve.Crypt.package.pkg_core_definition]
prog_valid [projection, in SSProve.Crypt.package.pkg_core_definition]
project [definition, in SSProve.Mon.Monoid]
ProjectionsFunctors [section, in SSProve.Relational.OrderEnrichedCategory]
ProjectionsFunctors [section, in SSProve.Relational.Category]
project_embed_id [lemma, in SSProve.Mon.Monoid]
projl [definition, in SSProve.Relational.EnrichedSetting]
projr [definition, in SSProve.Relational.EnrichedSetting]
proof_irrelevance [definition, in SSProve.Crypt.Axioms]
_ \O _ [notation, in SSProve.Crypt.rhl_semantics.more_categories.LaxComp]
Proper_rlmm_comp [section, in SSProve.Crypt.rhl_semantics.more_categories.LaxComp]
prove_code [lemma, in SSProve.Crypt.package.pkg_core_definition]
PRPCCA [library]
'ciph (package_scope) [notation, in SSProve.Crypt.examples.PRPCCA]
pack_type:'ciph [notation, in SSProve.Crypt.examples.PRPCCA]
'key (package_scope) [notation, in SSProve.Crypt.examples.PRPCCA]
pack_type:'key [notation, in SSProve.Crypt.examples.PRPCCA]
'word (package_scope) [notation, in SSProve.Crypt.examples.PRPCCA]
pack_type:'word [notation, in SSProve.Crypt.examples.PRPCCA]
PRPCCA_example.l [variable, in SSProve.Crypt.examples.PRPCCA]
PRPCCA_example.n [variable, in SSProve.Crypt.examples.PRPCCA]
'set _ (package_scope) [notation, in SSProve.Crypt.examples.PRPCCA]
pack_type:'set _ [notation, in SSProve.Crypt.examples.PRPCCA]
PRPCCA_example [section, in SSProve.Crypt.examples.PRPCCA]
prp_epsilon [definition, in SSProve.Crypt.examples.PRPCCA]
Pr_eq [lemma, in SSProve.Crypt.rules.RulesStateProb]
Pr_op [definition, in SSProve.Crypt.package.pkg_advantage]
Pr_raw_func_code [definition, in SSProve.Crypt.package.pkg_advantage]
Pr_code [definition, in SSProve.Crypt.package.pkg_advantage]
Pr_eq_empty [lemma, in SSProve.Crypt.package.pkg_rhl]
psum_SDistr_unit [lemma, in SSProve.Crypt.rhl_semantics.only_prob.Couplings]
psum_coupling_right [lemma, in SSProve.Crypt.rhl_semantics.only_prob.Couplings]
psum_coupling_left [lemma, in SSProve.Crypt.rhl_semantics.only_prob.Couplings]
psum_exists [lemma, in SSProve.Crypt.package.pkg_rhl]
pt_in_zero_points [lemma, in SSProve.Crypt.examples.PolynomialUtils]
pure [definition, in SSProve.Crypt.rules.RulesStateProb]
put [definition, in SSProve.Mon.MonadExamples]
putr [constructor, in SSProve.Crypt.package.pkg_core_definition]
putStP [definition, in SSProve.Crypt.rhl_semantics.state_prob.StateTransformingLaxMorph]
putt [constructor, in SSProve.Crypt.rhl_semantics.state_prob.StateTransformingLaxMorph]
put_case [lemma, in SSProve.Crypt.package.pkg_rhl]
put_pre_cond_rem_rhs [lemma, in SSProve.Crypt.package.pkg_invariants]
put_pre_cond_rem_lhs [lemma, in SSProve.Crypt.package.pkg_invariants]
put_pre_cond_triple_rhs [lemma, in SSProve.Crypt.package.pkg_invariants]
put_pre_cond_couple_rhs [lemma, in SSProve.Crypt.package.pkg_invariants]
put_pre_cond_couple_lhs [lemma, in SSProve.Crypt.package.pkg_invariants]
put_pre_cond_conj [lemma, in SSProve.Crypt.package.pkg_invariants]
put_pre_cond_heap_ignore [lemma, in SSProve.Crypt.package.pkg_invariants]
put_pre_cond [definition, in SSProve.Crypt.package.pkg_invariants]
P_AR [definition, in SSProve.Crypt.rhl_semantics.free_monad.FreeProbProg]
P_OP [definition, in SSProve.Crypt.rhl_semantics.free_monad.FreeProbProg]
p_pow_positive [instance, in SSProve.Crypt.examples.ShamirSecretSharing]
P_ltP [lemma, in SSProve.Crypt.jasmin_util]
P_leP [lemma, in SSProve.Crypt.jasmin_util]
p0 [definition, in SSProve.Crypt.examples.package_usage_example]
p1 [definition, in SSProve.Crypt.examples.package_usage_example]
p2 [definition, in SSProve.Crypt.examples.package_usage_example]

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)