Macros§
- always_
and_ equality_ n - always_
and_ equality_ n_ internal - always_
lift_ state_ and_ equality_ n - always_
lift_ state_ and_ equality_ n_ internal - always_
lift_ state_ weaken_ n - always_
lift_ state_ weaken_ n_ internal - combine_
spec_ entails_ always_ n - combine_
spec_ entails_ always_ n_ internal - entails_
always_ and_ n - entails_
always_ and_ n_ internal - entails_
always_ lift_ state_ and_ n - entails_
always_ lift_ state_ and_ n_ internal - entails_
and_ n - entails_
and_ n_ internal - implies_
new_ invariant_ n - implies_
new_ invariant_ n_ internal - invariant_
n - invariant_
n_ internal - leads_
to_ always_ combine_ n - leads_
to_ always_ combine_ n_ internal - leads_
to_ always_ combine_ n_ with_ equality - leads_
to_ always_ combine_ n_ with_ equality_ internal - leads_
to_ trans_ n - leads_
to_ trans_ n_ internal - or_
leads_ to_ combine_ and_ equality2 - or_
leads_ to_ combine_ n - or_
leads_ to_ combine_ n_ internal - stable_
and_ always_ n - stable_
and_ always_ n_ internal - stable_
and_ n - stable_
and_ n_ internal - state_
pred_ and - temp_
pred_ and - temp_
pred_ and_ internal - wf1_
by_ borrowing_ inv_ n
Functions§
- always_
and_ equality - always_
double_ equality - always_
implies_ forall_ intro - always_
implies_ preserved_ by_ always - always_
implies_ to_ leads_ to - always_
lift_ state_ and_ equality - always_
lift_ state_ weaken - always_
p_ is_ stable - always_
to_ always_ later - always_
weaken - eliminate_
always - entails_
always_ lift_ state_ and - entails_
always_ lift_ state_ and_ elim - entails_
and_ different_ temp - entails_
and_ equality - entails_
and_ temp - entails_
and_ temp_ reverse - entails_
implies_ leads_ to - entails_
implies_ temp_ reverse - entails_
not_ temp_ reverse - entails_
or_ temp - entails_
preserved_ by_ always - entails_
tla_ exists_ by_ witness - entails_
trans - entails_
trans_ by_ simplify - group_
tla_ rules - implies_
new_ invariant - implies_
tla_ exists_ by_ witness - implies_
tla_ exists_ intro - init_
invariant - leads_
to_ always_ combine - leads_
to_ always_ enhance - leads_
to_ always_ tla_ forall - leads_
to_ apply - leads_
to_ by_ borrowing_ inv - leads_
to_ framed_ by_ or - leads_
to_ rank_ step_ one - leads_
to_ rank_ step_ one_ usize - leads_
to_ self_ temp - leads_
to_ shortcut_ temp - leads_
to_ stable - leads_
to_ tla_ exists_ by_ witness - leads_
to_ tla_ exists_ intro - leads_
to_ trans - leads_
to_ weaken - lift_
state_ and_ equality - lift_
state_ exists_ absorb_ equality - lift_
state_ exists_ equality - lift_
state_ exists_ leads_ to_ case_ analysis - lift_
state_ exists_ leads_ to_ intro - lift_
state_ forall_ absorb_ equality - lift_
state_ implies_ equality - lift_
state_ not_ equality - lift_
state_ or_ equality - or_
leads_ to_ case_ analysis - or_
leads_ to_ combine - p_
leads_ to_ q_ is_ stable - pack_
conditions_ to_ spec - spec_
entails_ always_ tla_ forall - spec_
entails_ tla_ forall - stable_
and_ temp - state_
exists_ intro - state_
pred_ and_ apply_ equality - state_
pred_ implies_ apply_ equality - state_
pred_ not_ apply_ equality - state_
pred_ or_ apply_ equality - strengthen_
leads_ to_ with_ until - strengthen_
next - temp_
pred_ equality - tla_
exists_ leads_ to_ intro - tla_
forall_ a_ p_ leads_ to_ q_ a_ is_ stable - tla_
forall_ always_ equality - tla_
forall_ always_ equality_ variant - tla_
forall_ apply - transform_
leads_ to_ with_ until - unpack_
conditions_ from_ spec - use_
always_ tla_ forall - use_
tla_ forall - vacuous_
leads_ to - wf1
- wf1_
by_ borrowing_ inv - wf1_
variant_ temp