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 (notation)

pack_type:'set _ [in SSProve.Crypt.examples.PRFMAC]
_ == _ ::> (bool_scope) [in SSProve.Crypt.jasmin_util]
_ == _ ::> _ (bool_scope) [in SSProve.Crypt.jasmin_util]
_ ≤ _ (cmp_scope) [in SSProve.Crypt.jasmin_util]
_ <= _ (cmp_scope) [in SSProve.Crypt.jasmin_util]
_ < _ (cmp_scope) [in SSProve.Crypt.jasmin_util]
_ ∘ _ (package_scope) [in SSProve.Crypt.package.pkg_composition]
{ package _ #with _ } (package_scope) [in SSProve.Crypt.package.pkg_core_definition]
{ package _ } (package_scope) [in SSProve.Crypt.package.pkg_core_definition]
{ code _ #with _ } (package_scope) [in SSProve.Crypt.package.pkg_core_definition]
{ code _ } (package_scope) [in SSProve.Crypt.package.pkg_core_definition]
_ ≈₀ _ (package_scope) [in SSProve.Crypt.package.pkg_advantage]
_ ≈[ _ ] _ (package_scope) [in SSProve.Crypt.package.pkg_advantage]
#assert _ ;; _ (package_scope) [in SSProve.Crypt.package.pkg_distr]
#assert _ as _ ;; _ (package_scope) [in SSProve.Crypt.package.pkg_distr]
[ hints _ ; .. ; _ ] (package_scope) [in SSProve.Crypt.Prelude]
[ hints _ ] (package_scope) [in SSProve.Crypt.Prelude]
[ hints ] (package_scope) [in SSProve.Crypt.Prelude]
⊢ₛ _ ⦃ _ ⦄ (package_scope) [in SSProve.Crypt.package.pkg_rhl]
⊢ ⦃ _ ⦄ _ ≈ _ ⦃ _ ⦄ (package_scope) [in SSProve.Crypt.package.pkg_rhl]
r⊨ ⦃ _ ⦄ _ ≈ _ ⦃ _ ⦄ (package_scope) [in SSProve.Crypt.package.pkg_rhl]
'set _ (package_scope) [in SSProve.Crypt.examples.PRFMAC]
_ ⋊ _ (package_scope) [in SSProve.Crypt.package.pkg_invariants]
_ × _ (type_scope) [in SSProve.Mon.Base]
∑ _ .. _ , _ (type_scope) [in SSProve.Crypt.Prelude]
[ /\ _ , _ , _ , _ , _ , _ , _ , _ , _ & _ ] (type_scope) [in SSProve.Crypt.jasmin_util]
[ /\ _ , _ , _ , _ , _ , _ , _ , _ & _ ] (type_scope) [in SSProve.Crypt.jasmin_util]
[ /\ _ , _ , _ , _ , _ , _ , _ & _ ] (type_scope) [in SSProve.Crypt.jasmin_util]
[ /\ _ , _ , _ , _ , _ , _ & _ ] (type_scope) [in SSProve.Crypt.jasmin_util]
[ /\ _ , _ , _ , _ , _ & _ ] (type_scope) [in SSProve.Crypt.jasmin_util]
[ /\ _ , _ , _ , _ , _ & _ ] (type_scope) [in SSProve.Crypt.jasmin_util]
_ ⟦ _ ; _ ⟧ [in SSProve.Relational.EnrichedSetting]
_ ⨰r _ [in SSProve.Relational.EnrichedSetting]
_ ⨰ _ [in SSProve.Relational.EnrichedSetting]
_ <$> _ [in SSProve.Mon.SPropMonadicStructures]
_ |= _ [in SSProve.Relational.OrderEnrichedRelativeMonadExamples]
_ ⧕ _ [in SSProve.Mon.Monoid]
_ ⋅ _ [in SSProve.Mon.Monoid]
_ ⪷ _ [in SSProve.Relational.OrderEnrichedCategory]
_ ∙ _ [in SSProve.Relational.OrderEnrichedCategory]
_ ⦅ _ ; _ ⦆ [in SSProve.Relational.OrderEnrichedCategory]
_ =⟨ _ ⟩ _ [in SSProve.Mon.Base]
_ .π2 [in SSProve.Crypt.Prelude]
_ .π1 [in SSProve.Crypt.Prelude]
_ ∼ _ [in SSProve.Relational.Category]
_ ∙ _ [in SSProve.Relational.Category]
_ ⦅ _ ; _ ⦆ [in SSProve.Relational.Category]
_ >> _ [in SSProve.Crypt.jasmin_util]
_ >>= _ [in SSProve.Crypt.jasmin_util]
let%opt _ := _ in _ [in SSProve.Crypt.jasmin_util]
Let _ := _ in _ [in SSProve.Crypt.jasmin_util]
Let: _ := _ in _ [in SSProve.Crypt.jasmin_util]
!1 [in SSProve.Relational.EnrichedSetting]
'let%opt '_' := _ in _ [in SSProve.Crypt.jasmin_util]
( _ ; _ ; _ ; _ ; _ ; _ ) [in SSProve.Crypt.Prelude]
( _ ; _ ; _ ; _ ; _ ) [in SSProve.Crypt.Prelude]
( _ ; _ ; _ ; _ ) [in SSProve.Crypt.Prelude]
( _ ; _ ; _ ) [in SSProve.Crypt.Prelude]
( _ ; _ ) [in SSProve.Crypt.Prelude]
(:: _ , .. , _ & _ ) [in SSProve.Crypt.jasmin_util]
[ let _ ; .. ; _ ] [in SSProve.Crypt.Main]
[ let _ ] [in SSProve.Crypt.Main]
[ let ] [in SSProve.Crypt.Main]
{ _ : _ ⫳ _ } [in SSProve.Mon.Base]
{ _ : _ ∥ _ } [in SSProve.Mon.Base]
⟨ _ , _ ⟩ [in SSProve.Mon.Base]
⟪ _ | _ ⟫ [in SSProve.Relational.EnrichedSetting]

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)