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)

other

pack_type:'set _ [notation, in SSProve.Crypt.examples.PRFMAC]
_ == _ ::> (bool_scope) [notation, in SSProve.Crypt.jasmin_util]
_ == _ ::> _ (bool_scope) [notation, in SSProve.Crypt.jasmin_util]
_ ≤ _ (cmp_scope) [notation, in SSProve.Crypt.jasmin_util]
_ <= _ (cmp_scope) [notation, in SSProve.Crypt.jasmin_util]
_ < _ (cmp_scope) [notation, in SSProve.Crypt.jasmin_util]
_ ∘ _ (package_scope) [notation, in SSProve.Crypt.package.pkg_composition]
{ package _ #with _ } (package_scope) [notation, in SSProve.Crypt.package.pkg_core_definition]
{ package _ } (package_scope) [notation, in SSProve.Crypt.package.pkg_core_definition]
{ code _ #with _ } (package_scope) [notation, in SSProve.Crypt.package.pkg_core_definition]
{ code _ } (package_scope) [notation, in SSProve.Crypt.package.pkg_core_definition]
_ ≈₀ _ (package_scope) [notation, in SSProve.Crypt.package.pkg_advantage]
_ ≈[ _ ] _ (package_scope) [notation, in SSProve.Crypt.package.pkg_advantage]
#assert _ ;; _ (package_scope) [notation, in SSProve.Crypt.package.pkg_distr]
#assert _ as _ ;; _ (package_scope) [notation, in SSProve.Crypt.package.pkg_distr]
[ hints _ ; .. ; _ ] (package_scope) [notation, in SSProve.Crypt.Prelude]
[ hints _ ] (package_scope) [notation, in SSProve.Crypt.Prelude]
[ hints ] (package_scope) [notation, in SSProve.Crypt.Prelude]
⊢ₛ _ ⦃ _ ⦄ (package_scope) [notation, in SSProve.Crypt.package.pkg_rhl]
⊢ ⦃ _ ⦄ _ ≈ _ ⦃ _ ⦄ (package_scope) [notation, in SSProve.Crypt.package.pkg_rhl]
r⊨ ⦃ _ ⦄ _ ≈ _ ⦃ _ ⦄ (package_scope) [notation, in SSProve.Crypt.package.pkg_rhl]
'set _ (package_scope) [notation, in SSProve.Crypt.examples.PRFMAC]
_ ⋊ _ (package_scope) [notation, in SSProve.Crypt.package.pkg_invariants]
_ × _ (type_scope) [notation, in SSProve.Mon.Base]
∑ _ .. _ , _ (type_scope) [notation, in SSProve.Crypt.Prelude]
[ /\ _ , _ , _ , _ , _ , _ , _ , _ , _ & _ ] (type_scope) [notation, in SSProve.Crypt.jasmin_util]
[ /\ _ , _ , _ , _ , _ , _ , _ , _ & _ ] (type_scope) [notation, in SSProve.Crypt.jasmin_util]
[ /\ _ , _ , _ , _ , _ , _ , _ & _ ] (type_scope) [notation, in SSProve.Crypt.jasmin_util]
[ /\ _ , _ , _ , _ , _ , _ & _ ] (type_scope) [notation, in SSProve.Crypt.jasmin_util]
[ /\ _ , _ , _ , _ , _ & _ ] (type_scope) [notation, in SSProve.Crypt.jasmin_util]
[ /\ _ , _ , _ , _ , _ & _ ] (type_scope) [notation, in SSProve.Crypt.jasmin_util]
_ ⟦ _ ; _ ⟧ [notation, in SSProve.Relational.EnrichedSetting]
_ ⨰r _ [notation, in SSProve.Relational.EnrichedSetting]
_ ⨰ _ [notation, in SSProve.Relational.EnrichedSetting]
_ <$> _ [notation, in SSProve.Mon.SPropMonadicStructures]
_ |= _ [notation, in SSProve.Relational.OrderEnrichedRelativeMonadExamples]
_ ⧕ _ [notation, in SSProve.Mon.Monoid]
_ ⋅ _ [notation, in SSProve.Mon.Monoid]
_ ⪷ _ [notation, in SSProve.Relational.OrderEnrichedCategory]
_ ∙ _ [notation, in SSProve.Relational.OrderEnrichedCategory]
_ ⦅ _ ; _ ⦆ [notation, in SSProve.Relational.OrderEnrichedCategory]
_ =⟨ _ ⟩ _ [notation, in SSProve.Mon.Base]
_ .π2 [notation, in SSProve.Crypt.Prelude]
_ .π1 [notation, in SSProve.Crypt.Prelude]
_ ∼ _ [notation, in SSProve.Relational.Category]
_ ∙ _ [notation, in SSProve.Relational.Category]
_ ⦅ _ ; _ ⦆ [notation, in SSProve.Relational.Category]
_ >> _ [notation, in SSProve.Crypt.jasmin_util]
_ >>= _ [notation, in SSProve.Crypt.jasmin_util]
let%opt _ := _ in _ [notation, in SSProve.Crypt.jasmin_util]
Let _ := _ in _ [notation, in SSProve.Crypt.jasmin_util]
Let: _ := _ in _ [notation, in SSProve.Crypt.jasmin_util]
!1 [notation, in SSProve.Relational.EnrichedSetting]
'let%opt '_' := _ in _ [notation, in SSProve.Crypt.jasmin_util]
( _ ; _ ; _ ; _ ; _ ; _ ) [notation, in SSProve.Crypt.Prelude]
( _ ; _ ; _ ; _ ; _ ) [notation, in SSProve.Crypt.Prelude]
( _ ; _ ; _ ; _ ) [notation, in SSProve.Crypt.Prelude]
( _ ; _ ; _ ) [notation, in SSProve.Crypt.Prelude]
( _ ; _ ) [notation, in SSProve.Crypt.Prelude]
(:: _ , .. , _ & _ ) [notation, in SSProve.Crypt.jasmin_util]
[ let _ ; .. ; _ ] [notation, in SSProve.Crypt.Main]
[ let _ ] [notation, in SSProve.Crypt.Main]
[ let ] [notation, in SSProve.Crypt.Main]
{ _ : _ ⫳ _ } [notation, in SSProve.Mon.Base]
{ _ : _ ∥ _ } [notation, in SSProve.Mon.Base]
⟨ _ , _ ⟩ [notation, in SSProve.Mon.Base]
⟪ _ | _ ⟫ [notation, in SSProve.Relational.EnrichedSetting]
Φ1' [abbreviation, in SSProve.Crypt.rhl_semantics.more_categories.TransformingLaxMorph]
Φ2' [abbreviation, in SSProve.Crypt.rhl_semantics.more_categories.TransformingLaxMorph]
Ω [definition, in SSProve.Mon.MonadExamples]
α [abbreviation, in SSProve.Crypt.rhl_semantics.more_categories.TransformingLaxMorph]
α [abbreviation, in SSProve.Relational.RelativeMonads]
β [abbreviation, in SSProve.Crypt.rhl_semantics.more_categories.TransformingLaxMorph]
η [abbreviation, in SSProve.Crypt.rhl_semantics.more_categories.InitialRelativeMonad]
η [abbreviation, in SSProve.Crypt.rhl_semantics.more_categories.LaxMorphismOfRelAdjunctions]
η [abbreviation, in SSProve.Crypt.rhl_semantics.free_monad.UniversalFreeMap]
η [abbreviation, in SSProve.Crypt.rules.RulesStateProb]
η [abbreviation, in SSProve.Relational.OrderEnrichedRelativeMonadExamples]
η [abbreviation, in SSProve.Relational.OrderEnrichedRelativeMonadExamples]
η [abbreviation, in SSProve.Relational.OrderEnrichedCategory]
η [abbreviation, in SSProve.Crypt.rhl_semantics.more_categories.TransformingLaxMorph]
η [abbreviation, in SSProve.Crypt.rhl_semantics.more_categories.TransformingLaxMorph]
η [abbreviation, in SSProve.Relational.RelativeMonads]
η [abbreviation, in SSProve.Relational.RelativeMonads]
η [abbreviation, in SSProve.Relational.RelativeMonads]
η [abbreviation, in SSProve.Crypt.rhl_semantics.more_categories.OrderEnrichedRelativeAdjunctions]
θ [definition, in SSProve.Crypt.rules.RulesStateProb]
θ [definition, in SSProve.Crypt.rhl_semantics.only_prob.Theta_exCP]
θbind [lemma, in SSProve.Relational.Commutativity]
θProb [definition, in SSProve.Mon.FiniteProbabilities]
θret [lemma, in SSProve.Relational.Commutativity]
θ_dens_OF_θ0_c_sample_s0 [lemma, in SSProve.Crypt.rules.RulesStateProb]
θ_dens_OF_θ0_sample_c_s0 [lemma, in SSProve.Crypt.rules.RulesStateProb]
θ_dens_vs_bind' [lemma, in SSProve.Crypt.rules.RulesStateProb]
θ_dens [definition, in SSProve.Crypt.rules.RulesStateProb]
θ_morph [definition, in SSProve.Crypt.rhl_semantics.only_prob.Theta_exCP]
θ0 [definition, in SSProve.Crypt.rules.RulesStateProb]
θ0 [definition, in SSProve.Crypt.rhl_semantics.only_prob.Theta_exCP]
θ0_OF_c_sample_s0 [lemma, in SSProve.Crypt.rules.RulesStateProb]
θ0_OF_sample_c_s0 [lemma, in SSProve.Crypt.rules.RulesStateProb]
θ0_of_sample [lemma, in SSProve.Crypt.rules.RulesStateProb]
θ0_sample_c_vs_s0 [lemma, in SSProve.Crypt.rules.RulesStateProb]
θ0_c_sample_vs_s0 [lemma, in SSProve.Crypt.rules.RulesStateProb]
θ0_vs_c_sample [lemma, in SSProve.Crypt.rules.RulesStateProb]
θ0_vs_sample_c [lemma, in SSProve.Crypt.rules.RulesStateProb]
θ0_vs_bind [lemma, in SSProve.Crypt.rules.RulesStateProb]
θ1 [abbreviation, in SSProve.Relational.OrderEnrichedRelativeMonadExamples]
θ2 [abbreviation, in SSProve.Relational.OrderEnrichedRelativeMonadExamples]
μ [abbreviation, in SSProve.Relational.RelativeMonads]
μ [abbreviation, in SSProve.Relational.RelativeMonads]
πl [abbreviation, in SSProve.Relational.Rel]
πr [abbreviation, in SSProve.Relational.Rel]
πw [abbreviation, in SSProve.Relational.Rel]
ϕ [definition, in SSProve.Crypt.rhl_semantics.only_prob.Theta_exCP]
ℓ [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)