Iris Porting Status

Lean: 09d27949abab · Rocq: ad2f70c4dbac

Total
7083		 Ported
1554		 Ignored
18		 Missing
5511		 Stale
3		 Progress
21.9%
Status:
▶algebra/504/2463 (20%)
▶agree.v[src]37/62 (60%)
Rocq NameStatusDetails
agree
agreeO
agreeO_map
agreeO_map_ne
agreeR
agree_cmra_mixin
agree_dist
agree_eq
agree_equiv
agree_map_morphism
agree_map_ne
agree_map_proper
agree_map_to_agree
agree_ofe_mixin
agree_op_instance
agree_op_proper
agree_pcore
agree_pcore_instance
agree_validN_instance
agree_validN_proper
agree_valid_instance
to_agree_op_inv
to_agree_op_invN
to_agree_op_inv_L
to_agree_proper
agreeRFIris.AgreeRF
agreeRF_contractiveIris.instRFunctorContractiveAgreeRFOfOFunctorContractive
agree_assocIris.Agree.op_assoc
agree_cancelableIris.instCancelableAgree
agree_cmra_discreteIris.instDiscreteAgreeOfDiscrete
agree_cmra_totalIris.instIsTotalAgree
agree_commIris.Agree.op_comm
agree_core_idIris.instCoreIdAgreeToAgree
agree_idempIris.Agree.idemp
agree_includedIris.Agree.included
agree_includedNIris.Agree.includedN
agree_mapIris.Agree.map
agree_map_composeIris.Agree.map_compose
agree_map_extIris.Agree.agree_map_ext
agree_map_idIris.Agree.map_id
agree_op_invIris.Agree.op_inv
agree_op_invNIris.Agree.op_invN
agree_op_neIris.Agree.op_neâ‚‚
agree_op_ne'Iris.Agree.op_ne
agree_validN_defIris.Agree.validN_iff
agree_validN_neIris.Agree.validN_ne
agree_valid_includedIris.Agree.valid_included
agree_valid_includedNIris.Agree.valid_includedN
elem_of_agreeIris.mem_of_agree
to_agreeIris.toAgree
to_agree_discreteIris.Agree.toAgree.is_discrete
to_agree_includedIris.Agree.toAgree_included
to_agree_includedNIris.Agree.toAgree_includedN
to_agree_included_LIris.Agree.toAgree_included_L
to_agree_injIris.Agree.toAgree_inj
to_agree_injNIris.Agree.toAgree_injN
to_agree_neIris.instNonExpansiveAgreeToAgree
to_agree_op_validIris.Agree.toAgree_op_valid_iff_equiv
to_agree_op_validNIris.Agree.toAgree_op_validN_iff_dist
to_agree_op_valid_LIris.toAgree_op_valid_iff_eq
to_agree_uninjIris.Agree.toAgree_uninj
to_agree_uninjNIris.Agree.toAgree_uninjN
▶auth.v[src]70/95 (74%)
Rocq NameStatusDetails
auth_auth
auth_auth_dfrac_is_op
auth_auth_proper
auth_cmra_discrete
auth_frag
auth_frag_is_op
auth_frag_op_validN_1
auth_frag_op_validN_2
auth_frag_op_valid_1
auth_frag_op_valid_2
auth_frag_proper
auth_frag_sep_homomorphism
auth_frag_validN_1
auth_frag_validN_2
auth_frag_valid_1
auth_frag_valid_2
auth_ofe_discrete
auth_view_rel
auth_view_rel_raw_mono
auth_view_rel_raw_unit
auth_view_rel_raw_valid
big_opL_auth_frag
big_opMS_auth_frag
big_opM_auth_frag
big_opS_auth_frag
authOAuth.instOFE
authRAuth.instCMRA
authRFAuth.AuthRF
authRF_contractiveAuth.instRFunctorContractiveAuthRF
authURAuth.instUCMRA
authURFAuth.AuthURF
authURF_contractiveAuth.instURFunctorContractiveAuthURF
auth_auth_core_idAuth.instCoreIdAuthDiscard
auth_auth_dfrac_includedAuth.auth_dfrac_included
auth_auth_dfrac_includedNAuth.auth_dfrac_includedN
auth_auth_dfrac_opAuth.auth_dfrac_op
auth_auth_dfrac_op_invAuth.auth_dfrac_op_inv
auth_auth_dfrac_op_invNAuth.auth_dfrac_op_invN
auth_auth_dfrac_op_inv_LAuth.auth_dfrac_op_inv_L
auth_auth_dfrac_op_validAuth.auth_dfrac_op_valid
auth_auth_dfrac_op_validNAuth.auth_dfrac_op_validN
auth_auth_dfrac_validAuth.auth_dfrac_valid
auth_auth_dfrac_validNAuth.auth_dfrac_validN
auth_auth_discreteAuth.auth_discrete
auth_auth_dist_injAuth.auth_dist_inj
auth_auth_includedAuth.auth_included
auth_auth_includedNAuth.auth_includedN
auth_auth_injAuth.auth_inj
auth_auth_neAuth.auth_ne
auth_auth_op_validAuth.auth_op_valid
auth_auth_op_validNAuth.auth_op_validN
auth_auth_validAuth.auth_valid
auth_auth_validNAuth.auth_validN
auth_both_core_discardedAuth.auth_both_core_discarded
auth_both_core_fracAuth.auth_both_core_frac
auth_both_core_idAuth.instCoreIdOpAuthDiscardFrag
auth_both_dfrac_includedAuth.auth_both_dfrac_included
auth_both_dfrac_includedNAuth.auth_both_dfrac_includedN
auth_both_dfrac_validAuth.both_dfrac_valid
auth_both_dfrac_validNAuth.both_dfrac_validN
auth_both_dfrac_valid_2Auth.auth_both_dfrac_valid_2
auth_both_dfrac_valid_discreteAuth.both_dfrac_valid_discrete
auth_both_includedAuth.auth_both_included
auth_both_includedNAuth.auth_both_includedN
auth_both_validAuth.auth_both_valid
auth_both_validNAuth.both_validN
auth_both_valid_2Auth.auth_both_valid_2
auth_both_valid_discreteAuth.auth_both_valid_discrete
auth_frag_coreAuth.frag_core
auth_frag_core_idAuth.instCoreIdFrag
auth_frag_discreteAuth.frag_discrete
auth_frag_dist_injAuth.frag_dist_inj
auth_frag_includedAuth.frag_included
auth_frag_includedNAuth.frag_includedN
auth_frag_injAuth.frag_inj
auth_frag_monoAuth.frag_inc_of_inc
auth_frag_neAuth.frag_ne
auth_frag_opAuth.frag_op
auth_frag_op_validAuth.frag_op_valid
auth_frag_op_validNAuth.frag_op_validN
auth_frag_validAuth.frag_valid
auth_frag_validNAuth.frag_validN
auth_local_updateAuth.auth_local_update
auth_updateAuth.auth_update
auth_updateP_auth_unpersistAuth.auth_updateP_auth_unpersist
auth_updateP_both_unpersistAuth.auth_updateP_both_unpersist
auth_update_allocAuth.auth_update_alloc
auth_update_authAuth.auth_update_auth
auth_update_auth_persistAuth.auth_update_auth_persist
auth_update_deallocAuth.auth_update_dealloc
auth_update_dfrac_allocAuth.auth_update_dfrac_alloc
auth_view_rel_discreteAuthViewRel.instIsViewRelDiscreteOfDiscreteOfDiscrete
auth_view_rel_existsAuthViewRel.authViewRel_exists_iff
auth_view_rel_rawAuthViewRel
auth_view_rel_unitAuthViewRel.authViewRel_unit_iff
▶big_op.v[src]63/140 (45%)
Rocq NameStatusDetails
big_opL
big_opL_commute1_L
big_opL_commute_L
big_opL_consZ_l
big_opL_consZ_r
big_opL_ne'
big_opL_opL
big_opL_opM
big_opL_opMS
big_opL_opS
big_opL_permutation'
big_opL_proper'
big_opL_zip_seq
big_opL_zip_seqZ
big_opM
big_opMS
big_opMS_aux
big_opMS_closed
big_opMS_commute
big_opMS_commute1
big_opMS_commute1_L
big_opMS_commute_L
big_opMS_def
big_opMS_delete
big_opMS_disj_union
big_opMS_elements
big_opMS_empty
big_opMS_ext
big_opMS_gen_proper
big_opMS_insert
big_opMS_ne
big_opMS_ne'
big_opMS_op
big_opMS_opL
big_opMS_opM
big_opMS_opMS
big_opMS_opS
big_opMS_proper
big_opMS_proper'
big_opMS_singleton
big_opMS_unit
big_opMS_unseal
big_opM_aux
big_opM_commute1_L
big_opM_commute_L
big_opM_def
big_opM_dom
big_opM_gset_to_gmap
big_opM_kmap
big_opM_map_seq
big_opM_map_seqZ
big_opM_ne'
big_opM_opL
big_opM_opM
big_opM_opMS
big_opM_opS
big_opM_proper'
big_opM_unseal
big_opS
big_opS_aux
big_opS_commute1_L
big_opS_commute_L
big_opS_def
big_opS_delete
big_opS_filter'
big_opS_fn_insert
big_opS_fn_insert'
big_opS_list_to_set
big_opS_ne'
big_opS_opL
big_opS_opM
big_opS_opMS
big_opS_opS
big_opS_proper
big_opS_proper'
big_opS_set_map
big_opS_unseal
big_opL_appIris.Algebra.BigOpL.bigOpL_append_equiv
big_opL_bindIris.Algebra.BigOpL.bigOpL_flatMap_equiv
big_opL_closedIris.Algebra.BigOpL.bigOpL_closed
big_opL_commuteIris.Algebra.BigOpL.bigOpL_hom
big_opL_commute1Iris.Algebra.BigOpL.bigOpL_hom_weak
big_opL_consIris.Algebra.BigOpL.bigOpL_cons
big_opL_extIris.Algebra.BigOpL.bigOpL_ext
big_opL_fmapIris.Algebra.BigOpL.bigOpL_map_equiv
big_opL_gen_properIris.Algebra.BigOpL.bigOpL_gen_proper
big_opL_gen_proper_2Iris.Algebra.BigOpL.bigOpL_gen_proper_2
big_opL_neIris.Algebra.BigOpL.bigOpL_dist
big_opL_nilIris.Algebra.BigOpL.bigOpL_nil
big_opL_omapIris.Algebra.BigOpL.bigOpL_filterMap_equiv
big_opL_opIris.Algebra.BigOpL.bigOpL_op_equiv
big_opL_permutationIris.Algebra.BigOpL.bigOpL_equiv_of_perm
big_opL_properIris.Algebra.BigOpL.bigOpL_equiv
big_opL_proper_2Iris.Algebra.BigOpL.bigOpL_proper_2
big_opL_sep_zipIris.Algebra.BigOpL.bigOpL_zip_op_equiv
big_opL_sep_zip_withIris.Algebra.BigOpL.bigOpL_zipWith_op_equiv
big_opL_singletonIris.Algebra.BigOpL.bigOpL_singleton_equiv
big_opL_snocIris.Algebra.BigOpL.bigOpL_snoc_equiv
big_opL_take_dropIris.Algebra.BigOpL.bigOpL_take_drop_equiv
big_opL_unitIris.Algebra.BigOpL.bigOpL_const_unit_equiv
big_opM_closedIris.Algebra.BigOpM.bigOpM_closed
big_opM_commuteIris.Algebra.BigOpM.bigOpM_hom
big_opM_commute1Iris.Algebra.BigOpM.bigOpM_weak_hom
big_opM_deleteIris.Algebra.BigOpM.bigOpM_delete_equiv
big_opM_emptyIris.Algebra.BigOpM.bigOpM_empty
big_opM_extIris.Algebra.BigOpM.bigOpM_ext
big_opM_filter'Iris.Algebra.BigOpM.bigOpM_filter_equiv
big_opM_fmapIris.Algebra.BigOpM.bigOpM_map_equiv
big_opM_fn_insertIris.Algebra.BigOpM.bigOpM_fn_insert_equiv
big_opM_fn_insert'Iris.Algebra.BigOpM.bigOpM_fn_insert_equiv'
big_opM_gen_properIris.Algebra.BigOpM.bigOpM_gen_proper
big_opM_gen_proper_2Iris.Algebra.BigOpM.bigOpM_gen_proper_2
big_opM_insertIris.Algebra.BigOpM.bigOpM_insert_equiv
big_opM_insert_deleteIris.Algebra.BigOpM.bigOpM_insert_delete_equiv
big_opM_insert_overrideIris.Algebra.BigOpM.bigOpM_insert_override_equiv
big_opM_list_to_mapIris.Algebra.BigOpM.bigOpM_ofList_equiv
big_opM_map_to_listIris.Algebra.BigOpM.bigOpM_toList_equiv
big_opM_neIris.Algebra.BigOpM.bigOpM_dist
big_opM_omapIris.Algebra.BigOpM.bigOpM_filterMap_equiv
big_opM_opIris.Algebra.BigOpM.bigOpM_op_equiv
big_opM_properIris.Algebra.BigOpM.bigOpM_proper
big_opM_proper_2Iris.Algebra.BigOpM.bigOpM_proper_2
big_opM_sep_zipIris.Algebra.BigOpM.bigOpM_sep_zip_equiv
big_opM_sep_zip_withIris.Algebra.BigOpM.bigOpM_sep_zipWith_equiv
big_opM_singletonIris.Algebra.BigOpM.bigOpM_singleton_equiv
big_opM_unionIris.Algebra.BigOpM.bigOpM_union_equiv
big_opM_unitIris.Algebra.BigOpM.bigOpM_const_unit_equiv
big_opS_closedIris.Algebra.BigOpS.bigOpS_closed
big_opS_commuteIris.Algebra.BigOpS.hom
big_opS_commute1Iris.Algebra.BigOpS.hom_weak
big_opS_elementsIris.Algebra.BigOpS.bigOpS_bigOpL
big_opS_emptyIris.Algebra.BigOpS.bigOpS_empty
big_opS_extIris.Algebra.BigOpS.bigOpS_ext
big_opS_gen_properIris.Algebra.BigOpS.bigOpS_gen_proper
big_opS_insertIris.Algebra.BigOpS.bigOpS_insert
big_opS_neIris.Algebra.BigOpS.bigOpS_dist
big_opS_opIris.Algebra.BigOpS.bigOpS_op_equiv
big_opS_singletonIris.Algebra.BigOpS.bigOpS_singleton
big_opS_unionIris.Algebra.BigOpS.bigOpS_union
big_opS_unitIris.Algebra.BigOpS.bigOpS_const_unit
▶cmra.v[src]176/364 (48%)
Rocq NameStatusDetails
Cancelable_proper
CmraMixin
Empty_setR
Empty_set_cancelable
Empty_set_cmra_discrete
Empty_set_cmra_mixin
Empty_set_core_id
Empty_set_op_instance
Empty_set_pcore_instance
Empty_set_validN_instance
Empty_set_valid_instance
IdFree_proper
Op
PCore
RAMixin
Some_core
Some_core_id
Some_includedN_1
Some_includedN_2
Some_includedN_is_Some
Some_includedN_mono
Some_includedN_refl
Some_included_1
Some_included_2
Some_included_is_Some
Some_included_mono
Some_included_refl
Some_op
Some_pair_included
Some_pair_includedN
Some_pair_includedN_l
Some_pair_includedN_r
Some_pair_includedN_total_1
Some_pair_includedN_total_2
Some_pair_included_l
Some_pair_included_r
Some_pair_included_total_1
Some_pair_included_total_2
Some_valid
Some_validN
UcmraMixin
Unit
Valid
ValidN
cmra_assoc
cmra_comm
cmra_core_proper
cmra_extend
cmra_includedN_preorder
cmra_includedN_proper
cmra_included_preorder
cmra_mixin_of'
cmra_mono'
cmra_monoN'
cmra_monoid
cmra_morphism_compose
cmra_ofeO
cmra_opM_fmap_Some
cmra_opM_ne
cmra_opM_opM_assoc_L
cmra_opM_opM_swap
cmra_opM_opM_swap_L
cmra_opM_proper
cmra_op_ne
cmra_op_ne'
cmra_pcore_idemp
cmra_pcore_l
cmra_pcore_ne
cmra_total_mixin
cmra_transport
cmra_transport_core
cmra_transport_core_id
cmra_transport_discrete
cmra_transport_ne
cmra_transport_op
cmra_transport_proper
cmra_transport_trans
cmra_transport_valid
cmra_transport_validN
cmra_validN_lt
cmra_validN_ne
cmra_validN_op_l
cmra_validN_proper
cmra_valid_validN
constURF
constURF_contractive
discrete_cmra_discrete
discrete_cmra_mixin
discrete_fun_cmra_mixin
discrete_fun_included_spec
discrete_fun_included_spec_1
discrete_fun_lookup_core
discrete_fun_lookup_empty
discrete_fun_lookup_op
discrete_fun_map_cmra_morphism
discrete_fun_op_instance
discrete_fun_pcore_instance
discrete_fun_ucmra_mixin
discrete_fun_unit_discrete
discrete_fun_unit_instance
discrete_fun_validN_instance
discrete_fun_valid_instance
discrete_validN_instance
exclusiveN_Some_l
exclusiveN_Some_r
exclusive_Some_l
exclusive_Some_r
id_free_ne
inj_cmra_mixin_restrict_validity
is_Some_included
is_Some_includedN
iso_cmra_mixin
iso_cmra_mixin_restrict_validity
op_None
op_None_left_id
op_None_right_id
op_is_Some
optionRF
optionRF_contractive
option_cmra_mixin
option_core_id
option_fmap_cmra_morphism
option_fmap_mono
option_op_instance
option_pcore_instance
option_ucmra_mixin
option_unit_instance
option_validN_instance
option_valid_instance
pair_cancelable
pair_core
pair_core_id
pair_exclusive_l
pair_exclusive_r
pair_id_free_l
pair_id_free_r
pair_included
pair_op
pair_op_1
pair_op_1_L
pair_op_2
pair_op_2_L
pair_pcore
pair_split
pair_split_L
pair_valid
pair_validN
pcore_Some
prodUR
prodURF
prodURF_contractive
prod_cmra_mixin
prod_cmra_total
prod_included
prod_includedN
prod_op_instance
prod_pcore_Some
prod_pcore_Some'
prod_pcore_instance
prod_ucmra_mixin
prod_unit_instance
prod_validN_instance
prod_valid_instance
rFunctor_apply
rFunctor_oFunctor_compose
rFunctor_oFunctor_compose_contractive_1
rFunctor_oFunctor_compose_contractive_2
ra_total_mixin
ucmra_cmraR
ucmra_ofeO
ucmra_pcore_unit
ucmra_unit_left_id
ucmra_unit_valid
unitUR
unit_cancelable
unit_cmra_discrete
unit_cmra_mixin
unit_core_id
unit_op_instance
unit_pcore_instance
unit_ucmra_mixin
unit_unit_instance
unit_validN_instance
unit_valid_instance
urFunctor_apply
urFunctor_oFunctor_compose
urFunctor_oFunctor_compose_contractive_1
urFunctor_oFunctor_compose_contractive_2
CancelableIris.CMRA.Cancelable
CmraDiscreteIris.CMRA.Discrete
CmraMorphismIris.CMRA.Hom
CmraTotalIris.CMRA.IsTotal
CoreIdIris.CMRA.CoreId
CoreId_properIris.CMRA.coreId_iff
ExclusiveIris.CMRA.Exclusive
Exclusive_properIris.CMRA.exclusive_iff
IdFreeIris.CMRA.IdFree
Some_includedIris.Option.some_inc_some_iff
Some_includedNIris.Option.some_incN_some_iff
Some_includedN_exclusiveIris.Option.dist_of_inc_exclusive
Some_includedN_opMIris.Option.some_incN_some_iff_opM
Some_includedN_totalIris.Option.some_incN_some_iff_isTotal
Some_included_exclusiveIris.Option.eqv_of_inc_exclusive
Some_included_opMIris.Option.some_inc_some_iff_opM
Some_included_totalIris.Option.some_inc_some_iff_isTotal
Some_op_opMIris.Option.some_op_opM
cancelableIris.CMRA.cancelable
cancelable_SomeIris.Option.instCancelableOptionSomeOfIdFree
cancelable_opIris.CMRA.cancelable_op
cancelable_properIris.CMRA.cancelable_iff
cmraIris.CMRA
cmra_assoc_LIris.CMRA.assoc_L
cmra_comm_LIris.CMRA.comm_L
cmra_core_core_idIris.CMRA.instCoreIdCore
cmra_core_dupIris.CMRA.core_op_core
cmra_core_dup_LIris.CMRA.core_op_core_L
cmra_core_idempIris.CMRA.core_idem
cmra_core_idemp_LIris.CMRA.core_idem_L
cmra_core_lIris.CMRA.core_op
cmra_core_l_LIris.CMRA.core_op_L
cmra_core_monoIris.CMRA.core_mono
cmra_core_monoNIris.CMRA.core_incN_core
cmra_core_neIris.CMRA.core_ne
cmra_core_rIris.CMRA.op_core
cmra_core_r_LIris.CMRA.op_core_L
cmra_core_validIris.CMRA.valid_core
cmra_core_validNIris.CMRA.validN_core
cmra_discrete_included_iffIris.CMRA.inc_iff_incN
cmra_discrete_included_iff_0Iris.CMRA.inc_0_iff_incN
cmra_discrete_included_lIris.CMRA.discrete_inc_l
cmra_discrete_included_rIris.CMRA.discrete_inc_r
cmra_discrete_valid_iffIris.CMRA.valid_iff_validN'
cmra_discrete_valid_iff_0Iris.CMRA.valid_0_iff_validN
cmra_includedN_lIris.CMRA.incN_op_left
cmra_includedN_leIris.CMRA.incN_of_incN_le
cmra_includedN_neIris.CMRA.incN_iff
cmra_includedN_rIris.CMRA.incN_op_right
cmra_includedN_transIris.CMRA.incN_trans
cmra_included_coreIris.CMRA.core_inc_self
cmra_included_dist_lIris.CMRA.included_dist_l
cmra_included_includedNIris.CMRA.incN_of_inc
cmra_included_lIris.CMRA.inc_op_left
cmra_included_pcoreIris.CMRA.pcore_inc_self
cmra_included_properIris.CMRA.inc_iff
cmra_included_rIris.CMRA.inc_op_right
cmra_included_transIris.CMRA.inc_trans
cmra_monoIris.CMRA.op_mono
cmra_monoNIris.CMRA.op_monoN
cmra_monoN_lIris.CMRA.op_monoN_right
cmra_monoN_rIris.CMRA.op_monoN_left
cmra_mono_lIris.CMRA.op_mono_right
cmra_mono_rIris.CMRA.op_mono_left
cmra_morphism_coreIris.CMRA.Hom.core
cmra_morphism_idIris.CMRA.Hom.id
cmra_morphism_monotoneIris.CMRA.Hom.mono
cmra_morphism_monotoneNIris.CMRA.Hom.monoN
cmra_morphism_properIris.CMRA.Hom.eqv
cmra_morphism_validIris.CMRA.Hom.valid
cmra_opM_opM_assocIris.Option.opM_opM_assoc
cmra_op_discreteIris.CMRA.discrete_op
cmra_op_opM_assocIris.CMRA.op_opM_assoc
cmra_op_opM_assoc_LIris.CMRA.op_opM_assoc_L
cmra_op_proper'Iris.CMRA.op_eqv
cmra_pcore_coreIris.CMRA.pcore_eq_core
cmra_pcore_core_idIris.CMRA.CoreId.of_pcore_eq_some
cmra_pcore_dupIris.CMRA.pcore_op_self
cmra_pcore_dup'Iris.CMRA.pcore_op_self'
cmra_pcore_dup_LIris.CMRA.pcore_op_self_L
cmra_pcore_idemp'Iris.CMRA.pcore_idem'
cmra_pcore_idemp_LIris.CMRA.pcore_idem_L
cmra_pcore_l'Iris.CMRA.pcore_op_left'
cmra_pcore_l_LIris.CMRA.pcore_op_left_L
cmra_pcore_monoIris.CMRA.pcore_mono
cmra_pcore_mono'Iris.CMRA.pcore_mono'
cmra_pcore_monoN'Iris.CMRA.pcore_monoN'
cmra_pcore_ne'Iris.CMRA.instNonExpansiveOptionPcore
cmra_pcore_properIris.CMRA.pcore_proper
cmra_pcore_proper'Iris.CMRA.pcore_proper'
cmra_pcore_rIris.CMRA.pcore_op_right
cmra_pcore_r'Iris.CMRA.pcore_op_right'
cmra_pcore_r_LIris.CMRA.pcore_op_right_L
cmra_pcore_validIris.CMRA.pcore_valid
cmra_pcore_validNIris.CMRA.pcore_validN
cmra_unit_cmra_totalIris.CMRA.unit_total
cmra_validN_Some_includedNIris.Option.validN_of_incN_validN
cmra_validN_includedIris.CMRA.validN_of_inc
cmra_validN_includedNIris.CMRA.validN_of_incN
cmra_validN_leIris.CMRA.validN_of_le
cmra_validN_ne'Iris.CMRA.validN_iff
cmra_validN_op_rIris.CMRA.validN_op_right
cmra_valid_Some_includedIris.Option.valid_of_inc_valid
cmra_valid_includedIris.CMRA.valid_of_inc
cmra_valid_op_lIris.CMRA.valid_op_left
cmra_valid_op_rIris.CMRA.valid_op_right
cmra_valid_properIris.CMRA.valid_iff
constRFIris.COFE.OFunctor.constOF_RFunctor
constRF_contractiveIris.OFunctor.constOF_RFunctorContractive
coreIris.CMRA.core
core_id_coreIris.CMRA.core_eqv_self
core_id_core_LIris.CMRA.core_eq_self
core_id_dupIris.CMRA.op_self
core_id_dup_LIris.CMRA.core_id_dup_L
core_id_extractIris.CMRA.op_core_right_of_inc
core_id_totalIris.CMRA.coreId_iff_core_eqv_self
core_id_total_LIris.CMRA.coreId_iff_core_eq_self
discrete_cancelableIris.CMRA.discrete_cancelable
discrete_funRIris.cmraDiscreteFunO
discrete_funURIris.ucmraDiscreteFunO
discrete_funURFIris.urFunctorDiscreteFunOF
discrete_funURF_contractiveIris.DiscreteFunOF_URFC
discrete_id_freeIris.CMRA.discrete_id_free
empty_cancelableIris.CMRA.empty_cancelable
exclusiveN_lIris.CMRA.not_valid_exclN_op_left
exclusiveN_opMIris.CMRA.none_of_excl_valid_op
exclusiveN_rIris.CMRA.not_valid_exclN_op_right
exclusive_cancelableIris.CMRA.exclusive_cancelable
exclusive_id_freeIris.CMRA.exclusive_idFree
exclusive_includedIris.CMRA.not_valid_of_excl_inc
exclusive_includedNIris.CMRA.not_valid_of_exclN_inc
exclusive_lIris.CMRA.not_valid_excl_op_left
exclusive_rIris.CMRA.not_excl_op_right
id_freeN_lIris.CMRA.id_freeN_l
id_freeN_rIris.CMRA.id_freeN_r
id_free_lIris.CMRA.id_free_l
id_free_op_lIris.CMRA.idFree_op_l
id_free_op_rIris.CMRA.idFree_op_r
id_free_properIris.CMRA.idFree_iff
id_free_rIris.CMRA.id_free_r
includedIris.CMRA.Included
includedNIris.CMRA.IncludedN
opMIris.CMRA.op?
optionRIris.cmraOption
optionURIris.ucmraOption
optionURFIris.urFunctorOptionOF
optionURF_contractiveIris.urFunctorContractiveOptionOF
option_cancelableIris.Option.instCancelableOptionOfIdFree
option_cmra_discreteIris.Option.instDiscreteOption
option_includedIris.Option.inc_iff
option_includedNIris.Option.incN_iff
option_includedN_totalIris.Option.incN_iff_isTotal
option_included_totalIris.Option.inc_iff_isTotal
pair_includedNIris.Prod.incN_iff
prodRIris.Prod.cmraProd
prodRFIris.instRFunctorProdOF
prodRF_contractiveIris.instRFunctorContractiveProdOF
prod_cmra_discreteIris.Prod.instDiscreteProd
prod_map_cmra_morphismIris.Prod.mapC
rFunctorIris.RFunctor
rFunctorContractiveIris.RFunctorContractive
rFunctor_to_oFunctorIris.RFunctor.toOFunctor
rFunctor_to_oFunctor_contractiveIris.RFunctorContractive.toOFunctorContractive
ucmraIris.UCMRA
ucmra_unit_core_idIris.CMRA.unit_CoreId
ucmra_unit_leastIris.CMRA.inc_unit
ucmra_unit_leastNIris.CMRA.incN_unit
ucmra_unit_left_id_LIris.CMRA.unit_left_id_L
ucmra_unit_right_idIris.CMRA.unit_right_id
ucmra_unit_right_id_LIris.CMRA.unit_right_id_L
ucmra_unit_validNIris.CMRA.unit_validN
unitRIris.cmraUnit
urFunctorIris.URFunctor
urFunctorContractiveIris.URFunctorContractive
urFunctor_to_rFunctorIris.URFunctor.toRFunctor
urFunctor_to_rFunctor_contractiveIris.URFunctorContractive.toRFunctorContractive
▶cmra_big_op.v[src]0/4 (0%)
Rocq NameStatusDetails
big_opL_None
big_opMS_None
big_opM_None
big_opS_None
▶coPset.v[src]0/31 (0%)
Rocq NameStatusDetails
coPsetO
coPsetR
coPsetUR
coPset_cmra_discrete
coPset_core
coPset_disj
coPset_disjO
coPset_disjR
coPset_disjUR
coPset_disj_cmra_discrete
coPset_disj_included
coPset_disj_op_instance
coPset_disj_pcore_instance
coPset_disj_ra_mixin
coPset_disj_ucmra_mixin
coPset_disj_union
coPset_disj_unit_instance
coPset_disj_valid_instance
coPset_disj_valid_inv_l
coPset_disj_valid_op
coPset_included
coPset_local_update
coPset_op
coPset_opM
coPset_op_instance
coPset_pcore_instance
coPset_ra_mixin
coPset_ucmra_mixin
coPset_unit_instance
coPset_update
coPset_valid_instance
▶cofe_solver.v[src]0/45 (0%)
Rocq NameStatusDetails
solution
solver.A'
solver.A_cofe
solver.T
solver.coerce
solver.coerce_f
solver.coerce_id
solver.coerce_proper
solver.embed
solver.embed'
solver.embed_coerce
solver.embed_f
solver.embed_ne
solver.embed_tower
solver.f
solver.f_S
solver.f_tower
solver.ff
solver.ff_ff
solver.ff_tower
solver.fg
solver.fold
solver.fold_ne
solver.g_S
solver.g_coerce
solver.g_embed_coerce
solver.gf
solver.gg
solver.gg_gg
solver.gg_tower
solver.ggff
solver.project
solver.result
solver.tower
solver.tower_car_ne
solver.tower_chain
solver.tower_cofe
solver.tower_compl
solver.tower_dist
solver.tower_equiv
solver.tower_inhabited
solver.tower_ofe_mixin
solver.unfold
solver.unfold_chain
solver.unfold_ne
▶csum.v[src]50/70 (71%)
Rocq NameStatusDetails
Cinl_proper
Cinr_proper
csum
csumO
csumR
csum_bchain_l
csum_bchain_r
csum_cmra_mixin
csum_compl
csum_dist
csum_equiv
csum_lbcompl
csum_map_cmra_morphism
csum_ofe_mixin
csum_op_instance
csum_pcore_instance
csum_validN_instance
csum_valid_instance
maybe_Cinl
maybe_Cinr
Cinl_cancelableIris.Csum.instCancelableInl
Cinl_core_idIris.Csum.instCoreIdInl
Cinl_discreteIris.Csum.instDiscreteEInl
Cinl_exclusiveIris.Csum.instExclusiveInl
Cinl_id_freeIris.Csum.instIdFreeInl
Cinl_includedIris.Csum.inl_included
Cinl_injIris.Csum.inl_inj
Cinl_inj_distIris.Csum.inl_injN
Cinl_neIris.Csum.instNonExpansiveInl
Cinl_opIris.Csum.inl_op
Cinl_validIris.Csum.inl_valid
Cinr_cancelableIris.Csum.instCancelableInr
Cinr_core_idIris.Csum.instCoreIdInr
Cinr_discreteIris.Csum.instDiscreteEInr
Cinr_exclusiveIris.Csum.instExclusiveInr
Cinr_id_freeIris.Csum.instIdFreeInr
Cinr_includedIris.Csum.inr_included
Cinr_injIris.Csum.inr_inj
Cinr_inj_distIris.Csum.inr_injN
Cinr_neIris.Csum.instNonExpansiveInr
Cinr_opIris.Csum.inr_op
Cinr_validIris.Csum.inr_valid
CsumInvalid_includedIris.Csum.invalid_included
Some_csum_includedIris.Csum.some_included
Some_csum_includedNIris.Csum.some_includedN
csumO_mapIris.Csum.oMap
csumO_map_neIris.Csum.oMap_ne
csumRFIris.Csum.OF
csumRF_contractiveIris.Csum.instRFunctorContractiveOF
csum_chain_lIris.Csum.chainL
csum_chain_rIris.Csum.chainR
csum_cmra_discreteIris.Csum.instDiscrete_1
csum_cofeIris.Csum.instIsCOFE
csum_includedIris.Csum.included
csum_includedNIris.Csum.includedN
csum_leibnizIris.Csum.instLeibniz
csum_local_update_lIris.Csum.local_update_l
csum_local_update_rIris.Csum.local_update_r
csum_mapIris.Csum.map
csum_map_cmra_neIris.Csum.map_ne
csum_map_composeIris.Csum.map_compose
csum_map_extIris.Csum.map_ext
csum_map_idIris.Csum.map_id
csum_ofe_discreteIris.Csum.instDiscrete
csum_updateP'_lIris.Csum.updateP'_l
csum_updateP'_rIris.Csum.updateP'_r
csum_updateP_lIris.Csum.updateP_l
csum_updateP_rIris.Csum.updateP_r
csum_update_lIris.Csum.update_l
csum_update_rIris.Csum.update_r
▶dfrac.v[src]14/31 (45%)
Rocq NameStatusDetails
DfracBoth_inj
DfracOwn_inj
dfracO
dfracR
dfrac_countable
dfrac_discarded_included
dfrac_eq_dec
dfrac_is_op
dfrac_op_discarded
dfrac_op_instance
dfrac_op_own
dfrac_own_included
dfrac_pcore_instance
dfrac_ra_mixin
dfrac_valid
dfrac_valid_instance
dfrac_valid_own
dfracIris.DFrac
dfrac_cancelableIris.DFrac.instCancelableOwn
dfrac_cmra_discreteIris.DFrac.instDiscrete
dfrac_discard_updateIris.DFrac.DFrac.update_discard
dfrac_discarded_core_idIris.DFrac.instCoreIdDiscard
dfrac_full_exclusiveIris.DFrac.instExclusiveOwnOfNat
dfrac_inhabitedIris.DFrac.instInhabited
dfrac_own_id_freeIris.DFrac.instIdFreeOwn
dfrac_undiscard_updateIris.DFrac.DFrac.update_acquire
dfrac_valid_discardedIris.DFrac.valid_discard
dfrac_valid_own_1Iris.DFrac.valid_own_one
dfrac_valid_own_discardedIris.DFrac.valid_own_op_discard
dfrac_valid_own_lIris.DFrac.valid_own_op
dfrac_valid_own_rIris.DFrac.valid_op_own
▶dyn_reservation_map.v[src]0/48 (0%)
Rocq NameStatusDetails
DynReservationMap_discrete
DynReservationMap_ne
DynReservationMap_proper
dyn_reservation_map
dyn_reservation_mapO
dyn_reservation_mapR
dyn_reservation_mapUR
dyn_reservation_map_alloc
dyn_reservation_map_cmra_discrete
dyn_reservation_map_cmra_mixin
dyn_reservation_map_data
dyn_reservation_map_data_core_id
dyn_reservation_map_data_discrete
dyn_reservation_map_data_is_op
dyn_reservation_map_data_mono
dyn_reservation_map_data_ne
dyn_reservation_map_data_op
dyn_reservation_map_data_proj_ne
dyn_reservation_map_data_proj_proper
dyn_reservation_map_data_proj_validN
dyn_reservation_map_data_proper
dyn_reservation_map_data_valid
dyn_reservation_map_dist
dyn_reservation_map_empty_instance
dyn_reservation_map_equiv
dyn_reservation_map_included
dyn_reservation_map_ofe_discrete
dyn_reservation_map_ofe_mixin
dyn_reservation_map_op_instance
dyn_reservation_map_pcore_instance
dyn_reservation_map_reserve
dyn_reservation_map_reserve'
dyn_reservation_map_token
dyn_reservation_map_token_difference
dyn_reservation_map_token_discrete
dyn_reservation_map_token_proj_validN
dyn_reservation_map_token_union
dyn_reservation_map_token_valid
dyn_reservation_map_token_valid_op
dyn_reservation_map_ucmra_mixin
dyn_reservation_map_update
dyn_reservation_map_updateP
dyn_reservation_map_validN_eq
dyn_reservation_map_validN_instance
dyn_reservation_map_valid_eq
dyn_reservation_map_valid_instance
from_reservation_map
to_reservation_map
▶excl.v[src]0/40 (0%)
Rocq NameStatusDetails
ExclInvalid_discrete
ExclInvalid_included
Excl_discrete
Excl_dist_inj
Excl_included
Excl_includedN
Excl_inj
Excl_ne
Excl_proper
excl
exclO
exclO_map
exclO_map_ne
exclR
exclRF
exclRF_contractive
excl_cmra_discrete
excl_cmra_mixin
excl_cofe
excl_dist
excl_equiv
excl_exclusive
excl_included
excl_includedN
excl_leibniz
excl_map
excl_map_cmra_morphism
excl_map_compose
excl_map_ext
excl_map_id
excl_map_ne
excl_ofe_discrete
excl_ofe_mixin
excl_op_instance
excl_pcore_instance
excl_validN_instance
excl_validN_inv_l
excl_validN_inv_r
excl_valid_instance
maybe_Excl
▶frac.v[src]0/17 (0%)
Rocq NameStatusDetails
fracO
fracR
frac_cancelable
frac_cmra_discrete
frac_full_exclusive
frac_id_free
frac_included
frac_included_weak
frac_is_op
frac_op
frac_op_instance
frac_pcore_instance
frac_ra_mixin
frac_valid
frac_valid_1
frac_valid_instance
is_op_frac
▶functions.v[src]0/32 (0%)
Rocq NameStatusDetails
discrete_funO_ofe_discrete
discrete_funR_cmra_discrete
discrete_fun_insert
discrete_fun_insert_discrete
discrete_fun_insert_ne
discrete_fun_insert_proper
discrete_fun_insert_update
discrete_fun_insert_updateP
discrete_fun_insert_updateP'
discrete_fun_lookup_insert
discrete_fun_lookup_insert_ne
discrete_fun_lookup_singleton
discrete_fun_lookup_singleton_ne
discrete_fun_singleton
discrete_fun_singleton_core
discrete_fun_singleton_core_id
discrete_fun_singleton_discrete
discrete_fun_singleton_ne
discrete_fun_singleton_op
discrete_fun_singleton_proper
discrete_fun_singleton_unit
discrete_fun_singleton_update
discrete_fun_singleton_updateP
discrete_fun_singleton_updateP'
discrete_fun_singleton_updateP_empty
discrete_fun_singleton_updateP_empty'
discrete_fun_singleton_update_empty
discrete_fun_singleton_valid
discrete_fun_singleton_validN
discrete_fun_update
discrete_fun_updateP
discrete_fun_updateP'
▶gmap.v[src]0/126 (0%)
Rocq NameStatusDetails
alloc_local_update
alloc_singleton_local_update
alloc_unit_singleton_update
alloc_unit_singleton_updateP
alloc_unit_singleton_updateP'
alloc_updateP
alloc_updateP'
alloc_updateP_cofinite
alloc_updateP_cofinite'
alloc_updateP_strong
alloc_updateP_strong'
alloc_updateP_strong_dep
alloc_updateP_strong_dep'
alter_ne
big_opM_ne_2
big_opM_singletons
big_opS_gset_to_gmap
big_opS_gset_to_gmap_L
delete_local_update
delete_local_update_cancelable
delete_ne
delete_singleton_local_update
delete_singleton_local_update_cancelable
delete_update
delete_valid
delete_validN
dom_included
dom_op
gmapO
gmapOF
gmapOF_contractive
gmapO_leibniz
gmapO_map
gmapO_map_ne
gmapR
gmapRF
gmapRF_contractive
gmapUR
gmapURF
gmapURF_contractive
gmap_bchain
gmap_cancelable
gmap_chain
gmap_cmra_discrete
gmap_cmra_mixin
gmap_cofe
gmap_compl
gmap_core_id
gmap_core_id'
gmap_disjoint_ne
gmap_dist
gmap_dom_ne
gmap_empty_discrete
gmap_fmap_cmra_morphism
gmap_fmap_mono
gmap_fmap_ne
gmap_fmap_ne_ext
gmap_insert_discrete
gmap_lbcompl
gmap_local_update
gmap_lookup_discrete
gmap_ofe_discrete
gmap_ofe_mixin
gmap_op
gmap_op_empty_l_L
gmap_op_empty_r
gmap_op_instance
gmap_op_union
gmap_op_valid0_disjoint
gmap_op_valid_disjoint
gmap_pcore_instance
gmap_singleton_core_id
gmap_singleton_discrete
gmap_ucmra_mixin
gmap_union_dist_eq
gmap_union_ne
gmap_unit_instance
gmap_validN_instance
gmap_valid_instance
insert_alloc_local_update
insert_idN
insert_local_update
insert_ne
insert_op
insert_singleton_op
insert_update
insert_updateP
insert_updateP'
insert_valid
insert_validN
lookup_core
lookup_included
lookup_includedN
lookup_ne
lookup_op
lookup_opM
lookup_op_homomorphism
lookup_total_ne
lookup_validN_Some
lookup_valid_Some
map_fmap_ne
map_seq_ne
map_zip_with_ne
merge_ne
partial_alter_ne
singleton_cancelable
singleton_core
singleton_core'
singleton_core_total
singleton_included
singleton_includedN_l
singleton_included_exclusive_l
singleton_included_l
singleton_included_mono
singleton_included_total
singleton_is_op
singleton_local_update
singleton_local_update_any
singleton_ne
singleton_op
singleton_update
singleton_updateP
singleton_updateP'
singleton_valid
singleton_validN
union_with_ne
▶gmultiset.v[src]0/21 (0%)
Rocq NameStatusDetails
big_opMS_singletons
gmultisetO
gmultisetR
gmultisetUR
gmultiset_cancelable
gmultiset_cmra_discrete
gmultiset_core
gmultiset_included
gmultiset_local_update
gmultiset_local_update_alloc
gmultiset_local_update_dealloc
gmultiset_op
gmultiset_opM
gmultiset_op_instance
gmultiset_pcore_instance
gmultiset_ra_mixin
gmultiset_ucmra_mixin
gmultiset_unit_instance
gmultiset_update
gmultiset_validN_instance
gmultiset_valid_instance
▶gset.v[src]0/52 (0%)
Rocq NameStatusDetails
GSet_inj
big_opS_singletons
gsetO
gsetR
gsetUR
gset_cmra_discrete
gset_core
gset_core_id
gset_disj
gset_disjO
gset_disjR
gset_disjUR
gset_disj_alloc_empty_local_update
gset_disj_alloc_empty_updateP
gset_disj_alloc_empty_updateP'
gset_disj_alloc_empty_updateP_strong
gset_disj_alloc_empty_updateP_strong'
gset_disj_alloc_local_update
gset_disj_alloc_op_local_update
gset_disj_alloc_updateP
gset_disj_alloc_updateP'
gset_disj_alloc_updateP_strong
gset_disj_alloc_updateP_strong'
gset_disj_cmra_discrete
gset_disj_dealloc_empty_local_update
gset_disj_dealloc_local_update
gset_disj_dealloc_op_local_update
gset_disj_included
gset_disj_op_instance
gset_disj_pcore_instance
gset_disj_ra_mixin
gset_disj_ucmra_mixin
gset_disj_union
gset_disj_unit_instance
gset_disj_valid_instance
gset_disj_valid_inv_l
gset_disj_valid_op
gset_included
gset_local_update
gset_op
gset_opM
gset_op_instance
gset_pcore_instance
gset_ra_mixin
gset_ucmra_mixin
gset_unit_instance
gset_update
gset_valid_instance
set_unfold_gset_disj_included
set_unfold_gset_disj_valid_op
set_unfold_gset_eq
set_unfold_gset_included
▶lib/dfrac_agree.v[src]27/29 (93%)
Rocq NameStatusDetails
dfrac_agreeRF_contractive
to_dfrac_agree_proper
dfrac_agreeR_private.Iris.Algebra.Lib.DFracAgree.0.Iris.DFracAgree.DFracAgreeR
dfrac_agreeRF_private.Iris.Algebra.Lib.DFracAgree.0.Iris.DFracAgree.DFracAgreeRF
dfrac_agree_included_private.Iris.Algebra.Lib.DFracAgree.0.Iris.DFracAgree.included
dfrac_agree_includedN_private.Iris.Algebra.Lib.DFracAgree.0.Iris.DFracAgree.includedN
dfrac_agree_included_L_private.Iris.Algebra.Lib.DFracAgree.0.Iris.DFracAgree.included_L
dfrac_agree_op_private.Iris.Algebra.Lib.DFracAgree.0.Iris.DFracAgree.mk_op
dfrac_agree_op_valid_private.Iris.Algebra.Lib.DFracAgree.0.Iris.DFracAgree.op_valid
dfrac_agree_op_validN_private.Iris.Algebra.Lib.DFracAgree.0.Iris.DFracAgree.op_validN
dfrac_agree_op_valid_L_private.Iris.Algebra.Lib.DFracAgree.0.Iris.DFracAgree.op_valid_L
dfrac_agree_persist_private.Iris.Algebra.Lib.DFracAgree.0.Iris.DFracAgree.persist
dfrac_agree_unpersist_private.Iris.Algebra.Lib.DFracAgree.0.Iris.DFracAgree.unpersist
dfrac_agree_update_2_private.Iris.Algebra.Lib.DFracAgree.0.Iris.DFracAgree.updateâ‚‚
frac_agree_included_private.Iris.Algebra.Lib.DFracAgree.0.Iris.DFracAgree.Frac.included
frac_agree_includedN_private.Iris.Algebra.Lib.DFracAgree.0.Iris.DFracAgree.Frac.includedN
frac_agree_included_L_private.Iris.Algebra.Lib.DFracAgree.0.Iris.DFracAgree.Frac.included_L
frac_agree_op_private.Iris.Algebra.Lib.DFracAgree.0.Iris.DFracAgree.Frac.mk_op
frac_agree_op_valid_private.Iris.Algebra.Lib.DFracAgree.0.Iris.DFracAgree.Frac.op_valid
frac_agree_op_validN_private.Iris.Algebra.Lib.DFracAgree.0.Iris.DFracAgree.Frac.op_validN
frac_agree_op_valid_L_private.Iris.Algebra.Lib.DFracAgree.0.Iris.DFracAgree.Frac.op_valid_L
frac_agree_update_2_private.Iris.Algebra.Lib.DFracAgree.0.Iris.DFracAgree.Frac.updateâ‚‚
to_dfrac_agree_private.Iris.Algebra.Lib.DFracAgree.0.Iris.DFracAgree.mk
to_dfrac_agree_discrete_private.Iris.Algebra.Lib.DFracAgree.0.Iris.DFracAgree.mk_discrete
to_dfrac_agree_exclusive_private.Iris.Algebra.Lib.DFracAgree.0.Iris.DFracAgree.mk_exclusive
to_dfrac_agree_inj_private.Iris.Algebra.Lib.DFracAgree.0.Iris.DFracAgree.mk_inj
to_dfrac_agree_injN_private.Iris.Algebra.Lib.DFracAgree.0.Iris.DFracAgree.mk_injN
to_dfrac_agree_ne_private.Iris.Algebra.Lib.DFracAgree.0.Iris.DFracAgree.mk_ne
to_frac_agree_private.Iris.Algebra.Lib.DFracAgree.0.Iris.DFracAgree.Frac.mk
▶lib/excl_auth.v[src]20/24 (83%)
Rocq NameStatusDetails
excl_authRF_contractive
excl_authURF_contractive
excl_auth_auth_proper
excl_auth_frag_proper
excl_authRIris.ExclAuth.ExclAuthR
excl_authRF_private.Iris.Algebra.Lib.ExclAuth.0.Iris.ExclAuth.ExclAuthRF
excl_authURIris.ExclAuth.ExclAuthUR
excl_authURF_private.Iris.Algebra.Lib.ExclAuth.0.Iris.ExclAuth.ExclAuthURF
excl_auth_agree_private.Iris.Algebra.Lib.ExclAuth.0.Iris.ExclAuth.agree
excl_auth_agreeN_private.Iris.Algebra.Lib.ExclAuth.0.Iris.ExclAuth.agreeN
excl_auth_agree_L_private.Iris.Algebra.Lib.ExclAuth.0.Iris.ExclAuth.agree_L
excl_auth_authIris.ExclAuth.auth
excl_auth_auth_discrete_private.Iris.Algebra.Lib.ExclAuth.0.Iris.ExclAuth.auth_discrete
excl_auth_auth_ne_private.Iris.Algebra.Lib.ExclAuth.0.Iris.ExclAuth.auth_ne
excl_auth_auth_op_valid_private.Iris.Algebra.Lib.ExclAuth.0.Iris.ExclAuth.auth_op_valid
excl_auth_auth_op_validN_private.Iris.Algebra.Lib.ExclAuth.0.Iris.ExclAuth.auth_op_validN
excl_auth_fragIris.ExclAuth.frag
excl_auth_frag_discrete_private.Iris.Algebra.Lib.ExclAuth.0.Iris.ExclAuth.frag_discrete
excl_auth_frag_ne_private.Iris.Algebra.Lib.ExclAuth.0.Iris.ExclAuth.frag_ne
excl_auth_frag_op_valid_private.Iris.Algebra.Lib.ExclAuth.0.Iris.ExclAuth.frag_op_valid
excl_auth_frag_op_validN_private.Iris.Algebra.Lib.ExclAuth.0.Iris.ExclAuth.frag_op_validN
excl_auth_update_private.Iris.Algebra.Lib.ExclAuth.0.Iris.ExclAuth.update
excl_auth_valid_private.Iris.Algebra.Lib.ExclAuth.0.Iris.ExclAuth.valid
excl_auth_validN_private.Iris.Algebra.Lib.ExclAuth.0.Iris.ExclAuth.validN
▶lib/frac_auth.v[src]39/46 (85%)
Rocq NameStatusDetails
frac_authRF_contractive
frac_authUR
frac_authURF_contractive
frac_auth_auth_proper
frac_auth_frag_proper
frac_auth_is_op
frac_auth_is_op_core_id
frac_authRFracAuth
frac_authRF_private.Iris.Algebra.Lib.FracAuth.0.FracAuth.FracAuthF
frac_authURF_private.Iris.Algebra.Lib.FracAuth.0.FracAuth.FracAuthURF
frac_auth_agree_private.Iris.Algebra.Lib.FracAuth.0.FracAuth.agree
frac_auth_agreeN_private.Iris.Algebra.Lib.FracAuth.0.FracAuth.agreeN
frac_auth_agree_L_private.Iris.Algebra.Lib.FracAuth.0.FracAuth.agree_L
frac_auth_authFracAuth.auth
frac_auth_auth_dfrac_op_private.Iris.Algebra.Lib.FracAuth.0.FracAuth.auth_dfrac_op
frac_auth_auth_dfrac_op_valid_private.Iris.Algebra.Lib.FracAuth.0.FracAuth.auth_dfrac_op_valid
frac_auth_auth_dfrac_op_validN_private.Iris.Algebra.Lib.FracAuth.0.FracAuth.auth_dfrac_op_validN
frac_auth_auth_dfrac_valid_private.Iris.Algebra.Lib.FracAuth.0.FracAuth.auth_dfrac_valid
frac_auth_auth_dfrac_validN_private.Iris.Algebra.Lib.FracAuth.0.FracAuth.auth_dfrac_validN
frac_auth_auth_discrete_private.Iris.Algebra.Lib.FracAuth.0.FracAuth.auth_discrete
frac_auth_auth_ne_private.Iris.Algebra.Lib.FracAuth.0.FracAuth.auth_ne
frac_auth_auth_op_valid_private.Iris.Algebra.Lib.FracAuth.0.FracAuth.auth_op_valid
frac_auth_auth_op_validN_private.Iris.Algebra.Lib.FracAuth.0.FracAuth.auth_op_validN
frac_auth_auth_valid_private.Iris.Algebra.Lib.FracAuth.0.FracAuth.auth_valid
frac_auth_auth_validN_private.Iris.Algebra.Lib.FracAuth.0.FracAuth.auth_validN
frac_auth_dfrac_valid_private.Iris.Algebra.Lib.FracAuth.0.FracAuth.dfrac_valid
frac_auth_dfrac_validN_private.Iris.Algebra.Lib.FracAuth.0.FracAuth.dfrac_validN
frac_auth_fragFracAuth.frag
frac_auth_frag_discrete_private.Iris.Algebra.Lib.FracAuth.0.FracAuth.frag_discrete
frac_auth_frag_ne_private.Iris.Algebra.Lib.FracAuth.0.FracAuth.frag_ne
frac_auth_frag_op_private.Iris.Algebra.Lib.FracAuth.0.FracAuth.frag_op
frac_auth_frag_op_valid_private.Iris.Algebra.Lib.FracAuth.0.FracAuth.frag_op_valid
frac_auth_frag_op_validN_private.Iris.Algebra.Lib.FracAuth.0.FracAuth.frag_op_validN
frac_auth_frag_valid_private.Iris.Algebra.Lib.FracAuth.0.FracAuth.frag_valid
frac_auth_frag_validN_private.Iris.Algebra.Lib.FracAuth.0.FracAuth.frag_validN
frac_auth_included_private.Iris.Algebra.Lib.FracAuth.0.FracAuth.included
frac_auth_includedN_private.Iris.Algebra.Lib.FracAuth.0.FracAuth.includedN
frac_auth_includedN_total_private.Iris.Algebra.Lib.FracAuth.0.FracAuth.includedN_total
frac_auth_included_total_private.Iris.Algebra.Lib.FracAuth.0.FracAuth.included_total
frac_auth_update_private.Iris.Algebra.Lib.FracAuth.0.FracAuth.update
frac_auth_updateP_auth_unpersist_private.Iris.Algebra.Lib.FracAuth.0.FracAuth.updateP_auth_unpersist
frac_auth_updateP_both_unpersist_private.Iris.Algebra.Lib.FracAuth.0.FracAuth.updateP_both_unpersist
frac_auth_update_1_private.Iris.Algebra.Lib.FracAuth.0.FracAuth.update_full
frac_auth_update_auth_persist_private.Iris.Algebra.Lib.FracAuth.0.FracAuth.update_auth_persist
frac_auth_valid_private.Iris.Algebra.Lib.FracAuth.0.FracAuth.valid
frac_auth_validN_private.Iris.Algebra.Lib.FracAuth.0.FracAuth.validN
▶lib/gmap_view.v[src]0/62 (0%)
Rocq NameStatusDetails
gmap_viewO
gmap_viewR
gmap_viewRF
gmap_viewRF_contractive
gmap_viewUR
gmap_viewURF
gmap_viewURF_contractive
gmap_view_alloc
gmap_view_alloc_big
gmap_view_auth
gmap_view_auth_dfrac_is_op
gmap_view_auth_dfrac_op
gmap_view_auth_dfrac_op_inv
gmap_view_auth_dfrac_op_invN
gmap_view_auth_dfrac_op_valid
gmap_view_auth_dfrac_op_validN
gmap_view_auth_dfrac_valid
gmap_view_auth_dfrac_validN
gmap_view_auth_ne
gmap_view_auth_op_valid
gmap_view_auth_op_validN
gmap_view_auth_persist
gmap_view_auth_proper
gmap_view_auth_unpersist
gmap_view_auth_valid
gmap_view_both_dfrac_validN
gmap_view_both_dfrac_validN_total
gmap_view_both_dfrac_valid_discrete
gmap_view_both_dfrac_valid_discrete_total
gmap_view_both_valid
gmap_view_both_validN
gmap_view_cmra_discrete
gmap_view_delete
gmap_view_delete_big
gmap_view_frag
gmap_view_fragUR
gmap_view_frag_add
gmap_view_frag_core_id
gmap_view_frag_dfrac
gmap_view_frag_mut_is_op
gmap_view_frag_ne
gmap_view_frag_op
gmap_view_frag_op_valid
gmap_view_frag_op_validN
gmap_view_frag_persist
gmap_view_frag_proper
gmap_view_frag_unpersist
gmap_view_frag_valid
gmap_view_frag_validN
gmap_view_rel
gmap_view_rel_discrete
gmap_view_rel_exists
gmap_view_rel_lookup
gmap_view_rel_raw
gmap_view_rel_raw_mono
gmap_view_rel_raw_unit
gmap_view_rel_raw_valid
gmap_view_rel_unit
gmap_view_replace
gmap_view_replace_big
gmap_view_update
gmap_view_update_local
▶lib/gset_bij.v[src]0/32 (0%)
Rocq NameStatusDetails
bij_both_dfrac_valid
bij_both_valid
bij_view_included
gset_bij
gset_bijO
gset_bijR
gset_bijUR
gset_bij_auth
gset_bij_auth_dfrac_op
gset_bij_auth_dfrac_op_valid
gset_bij_auth_dfrac_valid
gset_bij_auth_empty_dfrac_valid
gset_bij_auth_empty_valid
gset_bij_auth_extend
gset_bij_auth_op_valid
gset_bij_auth_valid
gset_bij_elem
gset_bij_elem_agree
gset_bij_elem_core_id
gset_bij_view_rel
gset_bij_view_rel_discrete
gset_bij_view_rel_iff
gset_bij_view_rel_raw
gset_bij_view_rel_raw_mono
gset_bij_view_rel_raw_unit
gset_bij_view_rel_raw_valid
gset_bijective
gset_bijective_empty
gset_bijective_eq_iff
gset_bijective_extend
gset_bijective_pair
subseteq_gset_bijective
▶lib/mono_Z.v[src]0/24 (0%)
Rocq NameStatusDetails
mono_Z
mono_ZR
mono_ZUR
mono_Z_auth
mono_Z_auth_core_id
mono_Z_auth_dfrac_is_op
mono_Z_auth_dfrac_op
mono_Z_auth_dfrac_op_valid
mono_Z_auth_dfrac_valid
mono_Z_auth_lb_op
mono_Z_auth_op_valid
mono_Z_auth_persist
mono_Z_auth_unpersist
mono_Z_auth_valid
mono_Z_both_dfrac_valid
mono_Z_both_valid
mono_Z_included
mono_Z_lb
mono_Z_lb_core_id
mono_Z_lb_max_is_op
mono_Z_lb_mono
mono_Z_lb_op
mono_Z_lb_op_le_l
mono_Z_update
▶lib/mono_list.v[src]0/45 (0%)
Rocq NameStatusDetails
mono_listR
mono_listRF
mono_listRF_contractive
mono_listUR
mono_listURF
mono_listURF_contractive
mono_list_auth
mono_list_auth_core_id
mono_list_auth_dfrac_is_op
mono_list_auth_dfrac_op
mono_list_auth_dfrac_op_valid
mono_list_auth_dfrac_op_validN
mono_list_auth_dfrac_op_valid_L
mono_list_auth_dfrac_valid
mono_list_auth_dfrac_validN
mono_list_auth_lb_op
mono_list_auth_ne
mono_list_auth_op_valid
mono_list_auth_op_validN
mono_list_auth_persist
mono_list_auth_proper
mono_list_auth_unpersist
mono_list_auth_valid
mono_list_auth_validN
mono_list_both_dfrac_valid
mono_list_both_dfrac_validN
mono_list_both_dfrac_valid_L
mono_list_both_valid
mono_list_both_validN
mono_list_both_valid_L
mono_list_included
mono_list_lb
mono_list_lb_dist_inj
mono_list_lb_inj
mono_list_lb_mono
mono_list_lb_ne
mono_list_lb_op_l
mono_list_lb_op_r
mono_list_lb_op_valid
mono_list_lb_op_validN
mono_list_lb_op_valid_1_L
mono_list_lb_op_valid_2_L
mono_list_lb_op_valid_L
mono_list_lb_proper
mono_list_update
▶lib/mono_nat.v[src]0/24 (0%)
Rocq NameStatusDetails
mono_nat
mono_natR
mono_natUR
mono_nat_auth
mono_nat_auth_core_id
mono_nat_auth_dfrac_is_op
mono_nat_auth_dfrac_op
mono_nat_auth_dfrac_op_valid
mono_nat_auth_dfrac_valid
mono_nat_auth_lb_op
mono_nat_auth_op_valid
mono_nat_auth_persist
mono_nat_auth_unpersist
mono_nat_auth_valid
mono_nat_both_dfrac_valid
mono_nat_both_valid
mono_nat_included
mono_nat_lb
mono_nat_lb_core_id
mono_nat_lb_max_is_op
mono_nat_lb_mono
mono_nat_lb_op
mono_nat_lb_op_le_l
mono_nat_update
▶lib/ufrac_auth.v[src]0/35 (0%)
Rocq NameStatusDetails
ufrac_authR
ufrac_authRF
ufrac_authRF_contractive
ufrac_authUR
ufrac_authURF
ufrac_authURF_contractive
ufrac_auth_agree
ufrac_auth_agreeN
ufrac_auth_agree_L
ufrac_auth_auth
ufrac_auth_auth_discrete
ufrac_auth_auth_ne
ufrac_auth_auth_proper
ufrac_auth_auth_valid
ufrac_auth_auth_validN
ufrac_auth_frag
ufrac_auth_frag_discrete
ufrac_auth_frag_ne
ufrac_auth_frag_op
ufrac_auth_frag_op_valid
ufrac_auth_frag_op_validN
ufrac_auth_frag_proper
ufrac_auth_frag_valid
ufrac_auth_frag_validN
ufrac_auth_included
ufrac_auth_includedN
ufrac_auth_includedN_total
ufrac_auth_included_total
ufrac_auth_is_op
ufrac_auth_is_op_core_id
ufrac_auth_update
ufrac_auth_update_surplus
ufrac_auth_update_surplus_cancel
ufrac_auth_valid
ufrac_auth_validN
▶list.v[src]0/48 (0%)
Rocq NameStatusDetails
app_dist_eq
app_ne
big_opL_ne_2
cons_discrete
cons_dist_eq
cons_dist_inj
cons_ne
dist_Permutation
drop_ne
head_ne
imap_ne
last_ne
length_ne
listO
listOF
listOF_contractive
listO_map
listO_map_ne
list_alter_ne
list_bind_ne
list_compl_go
list_delete_ne
list_dist
list_dist_Forall2
list_dist_lookup
list_filter_ne
list_fmap_dist_inj
list_fmap_ext_ne
list_fmap_ne
list_insert_ne
list_inserts_ne
list_join_ne
list_lbcompl_go
list_lookup_ne
list_lookup_total_ne
list_ofe_discrete
list_ofe_mixin
list_omap_ne
list_singleton_dist_eq
nil_discrete
nil_dist_eq
option_list_ne
replicate_ne
resize_ne
reverse_ne
tail_ne
take_ne
zip_with_ne
▶local_updates.v[src]0/29 (0%)
Rocq NameStatusDetails
alloc_option_local_update
cancel_local_update
cancel_local_update_unit
core_id_local_update
delete_option_local_update
delete_option_local_update_cancelable
discrete_fun_local_update
exclusive_local_update
local_update
local_update_discrete
local_update_preorder
local_update_proper
local_update_total_valid
local_update_total_valid0
local_update_unital
local_update_unital_discrete
local_update_valid
local_update_valid0
op_local_update
op_local_update_discrete
op_local_update_frame
option_local_update
option_local_update_None
prod_local_update
prod_local_update'
prod_local_update_1
prod_local_update_2
replace_local_update
unit_local_update
▶max_prefix_list.v[src]0/28 (0%)
Rocq NameStatusDetails
max_prefix_list
max_prefix_listR
max_prefix_listRF
max_prefix_listRF_contractive
max_prefix_listUR
max_prefix_listURF
max_prefix_listURF_contractive
max_prefix_list_included_includedN
max_prefix_list_local_update
mono_list_lb_core_id
to_max_prefix_list
to_max_prefix_list_app
to_max_prefix_list_dist_inj
to_max_prefix_list_included
to_max_prefix_list_includedN
to_max_prefix_list_includedN_aux
to_max_prefix_list_included_L
to_max_prefix_list_inj
to_max_prefix_list_ne
to_max_prefix_list_op_l
to_max_prefix_list_op_r
to_max_prefix_list_op_valid
to_max_prefix_list_op_validN
to_max_prefix_list_op_validN_aux
to_max_prefix_list_op_valid_L
to_max_prefix_list_proper
to_max_prefix_list_valid
to_max_prefix_list_validN
▶monoid.v[src]0/8 (0%)
Rocq NameStatusDetails
Monoid
MonoidHomomorphism
MonoidOps
WeakMonoidHomomorphism
monoid_ops
monoid_proper
monoid_right_id
weak_monoid_homomorphism_proper
▶mra.v[src]0/30 (0%)
Rocq NameStatusDetails
auth_ucmra_mixin
mra
mraO
mraR
mraUR
mra_below
mra_below_to_mra
mra_cmra_discrete
mra_cmra_mixin
mra_cmra_total
mra_core_id
mra_equiv
mra_equiv_equiv
mra_idemp
mra_included
mra_local_update_get_frag
mra_local_update_grow
mra_op
mra_pcore
mra_unit
mra_valid
mra_validN
to_mra
to_mra_R_op
to_mra_equiv_inj
to_mra_included
to_mra_inj
to_mra_proper
to_mra_rel_inj
to_mra_rel_proper
▶numbers.v[src]0/88 (0%)
Rocq NameStatusDetails
ZR
ZUR
Z_cancelable
Z_cmra_discrete
Z_is_op
Z_local_update
Z_op
Z_op_instance
Z_pcore_instance
Z_ra_mixin
Z_ucmra_mixin
Z_unit_instance
Z_validN_instance
Z_valid_instance
max_Z
max_ZO
max_ZR
max_Z_cmra_discrete
max_Z_cmra_total
max_Z_core_id
max_Z_included
max_Z_is_op
max_Z_local_update
max_Z_op
max_Z_op_instance
max_Z_pcore_instance
max_Z_ra_mixin
max_Z_unit_instance
max_Z_validN_instance
max_Z_valid_instance
max_nat
max_natO
max_natR
max_natUR
max_nat_cmra_discrete
max_nat_core_id
max_nat_included
max_nat_is_op
max_nat_local_update
max_nat_op
max_nat_op_instance
max_nat_pcore_instance
max_nat_ra_mixin
max_nat_ucmra_mixin
max_nat_unit_instance
max_nat_validN_instance
max_nat_valid_instance
min_nat
min_natO
min_natR
min_nat_cmra_discrete
min_nat_core_id
min_nat_included
min_nat_is_op
min_nat_local_update
min_nat_op_instance
min_nat_op_min
min_nat_pcore_instance
min_nat_ra_mixin
min_nat_validN_instance
min_nat_valid_instance
natR
natUR
nat_cancelable
nat_cmra_discrete
nat_included
nat_is_op
nat_local_update
nat_op
nat_op_instance
nat_pcore_instance
nat_ra_mixin
nat_ucmra_mixin
nat_unit_instance
nat_validN_instance
nat_valid_instance
pos_cancelable
pos_cmra_discrete
pos_id_free
pos_included
pos_is_op
pos_op_add
pos_op_instance
pos_pcore_instance
pos_ra_mixin
pos_validN_instance
pos_valid_instance
positiveR
▶ofe.v[src]7/331 (2%)
Rocq NameStatusDetails
Cofe
Discrete
Discrete_proper
Dist
Empty_setO
Empty_set_cofe
Empty_set_dist
Empty_set_ofe_discrete
Empty_set_ofe_mixin
LimitPreserving
NO
Next_contractive
Next_inj
Next_uninj
None_discrete
OfeDiscrete
OfeMixin
PropO
Prop_equiv
Prop_equivalence
Some_discrete
Some_dist_inj
Some_ne
ZO
bchain
bchain_const
bchain_le
bchain_map
bchain_map_snd
bcompl
bcompl_ne
bfchain
bfchain_chain_unique
boolO
ccompose
ccompose_ne
ccompose_proper
cconst
chain
chain_const
chain_map
chain_map_snd
cid
compl_bchain_map
compl_chain_const
compl_chain_map
constOF
constOF_contractive
const_contractive
contractive_0
contractive_alt
contractive_dist_later_dist
contractive_ne
contractive_proper
conv_bcompl
conv_compl_le
curry3_ne
curry4_ne
curry_ne
discrete
discrete_cofe
discrete_dist
discrete_fun
discrete_funO
discrete_funOF
discrete_funOF_contractive
discrete_funO_map
discrete_funO_map_ne
discrete_fun_bchain
discrete_fun_chain
discrete_fun_cofe
discrete_fun_dist
discrete_fun_equiv
discrete_fun_lookup_discrete
discrete_fun_map
discrete_fun_map_compose
discrete_fun_map_ext
discrete_fun_map_id
discrete_fun_map_ne
discrete_fun_ofe_mixin
discrete_iff
discrete_iff_0
discrete_ofe_discrete
discrete_ofe_mixin
dist_None
dist_Some
dist_Some_inv_l
dist_Some_inv_l'
dist_Some_inv_r
dist_Some_inv_r'
dist_dist_later
dist_equivalence
dist_later
dist_later_0
dist_later_dist_lt
dist_later_equivalence
dist_le'
dist_lt
dist_ne
dist_pointwise_lt
dist_proper
dist_proper_2
equiv_dist
existT_ne
existT_ne_2
existT_proper
existT_proper_2
exist_ne
fixpoint
fixpointK
fixpointK_ind
fixpointK_ne
fixpointK_proper
fixpointK_unfold
fixpointK_unique
fixpoint_A
fixpoint_AA
fixpoint_AA_contractive
fixpoint_AB
fixpoint_AB_contractive
fixpoint_A_ne
fixpoint_A_proper
fixpoint_A_unfold
fixpoint_A_unique
fixpoint_B
fixpoint_B_ne
fixpoint_B_proper
fixpoint_B_unfold
fixpoint_B_unique
fixpoint_aux
fixpoint_bchain
fixpoint_bchain_go
fixpoint_chain
fixpoint_def
fixpoint_ind
fixpoint_ne
fixpoint_proper
fixpoint_unfold
fixpoint_unique
fixpoint_unseal
fmap_Some_dist
from_option_ne
fst_ne
idOF
inl_bchain
inl_chain
inl_discrete
inl_ne
inl_ne_inj
inr_bchain
inr_chain
inr_discrete
inr_ne
inr_ne_inj
is_Some_ne
iso_cofe
iso_cofe_subtype
iso_cofe_subtype'
iso_ofe_cong
iso_ofe_cong_contractive
iso_ofe_cong_ne
iso_ofe_mixin
iso_ofe_refl
iso_ofe_sym
iso_ofe_sym_ne
iso_ofe_trans
iso_ofe_trans_ne
later
laterO
laterOF
laterOF_contractive
laterO_map
laterO_map_contractive
later_car_anti_contractive
later_chain
later_cofe
later_dist
later_equiv
later_limit_bchain
later_map
later_map_Next
later_map_compose
later_map_ext
later_map_id
later_map_ne
later_map_ne'
later_map_proper
later_ofe_mixin
lbcompl_bchain_le
leibnizO_leibniz
limit_preserving_and
limit_preserving_bcompl
limit_preserving_const
limit_preserving_discrete
limit_preserving_equiv
limit_preserving_forall
limit_preserving_impl
limit_preserving_impl'
limit_preserving_sidx_finite
natO
ne_dist_later
ne_proper
ne_proper_2
oFunctor
oFunctorContractive
oFunctor_apply
oFunctor_oFunctor_compose
oFunctor_oFunctor_compose_contractive_1
oFunctor_oFunctor_compose_contractive_2
ofe
ofe_discrete_subrelation
ofe_equivalence
ofe_iso
ofe_isoO
ofe_iso_1_ne
ofe_iso_2_ne
ofe_iso_cofe
ofe_iso_dist
ofe_iso_equiv
ofe_iso_ofe_mixin
ofe_leibniz_subrelation
ofe_mixin_of'
ofe_mor
ofe_morO
ofe_morOF
ofe_morOF_contractive
ofe_morO_map
ofe_morO_map_ne
ofe_mor_bchain
ofe_mor_car_ne
ofe_mor_car_proper
ofe_mor_chain
ofe_mor_cofe
ofe_mor_compl
ofe_mor_dist
ofe_mor_equiv
ofe_mor_ext
ofe_mor_inhabited
ofe_mor_lbcompl
ofe_mor_map
ofe_mor_map_ne
ofe_mor_ofe_mixin
ofe_mor_proper
optionO
optionOF
optionOF_contractive
optionO_map
optionO_map_ne
option_bchain
option_chain
option_cofe
option_compl
option_dist
option_dist_Forall2
option_fmap_dist_inj
option_fmap_ne
option_lbcompl
option_mbind_ne
option_mjoin_ne
option_ofe_discrete
option_ofe_mixin
pair_dist
pair_dist_inj
pair_ne
positiveO
prodO
prodO_map_ne
prod_cofe
prod_discrete
prod_dist
prod_map_ne
prod_ofe_discrete
prod_ofe_mixin
projT1_ne
projT1_proper
projT2_ne
projT2_proper
sigO
sigTO
sigTOF
sigTOF_contractive
sigT_bchain_const_proj1
sigT_chain_const_proj1
sigT_cofe
sigT_compl
sigT_discrete
sigT_dist
sigT_dist_eq
sigT_dist_proj1
sigT_equiv
sigT_equiv_eq
sigT_equiv_eq_alt
sigT_equiv_proj1
sigT_lbcompl
sigT_map
sigT_ofe_discrete
sigT_ofe_mixin
sig_cofe
sig_dist
sig_dist_def
sig_equiv
sig_equiv_def
sig_ofe_discrete
snd_ne
sumO
sumOF
sumOF_contractive
sumO_map
sumO_map_ne
sum_cofe
sum_compl
sum_dist
sum_lbcompl
sum_map_ne
sum_ofe_discrete
sum_ofe_mixin
uncurry3_ne
uncurry4_ne
uncurry_ne
unitO
unit_cofe
unit_dist
unit_ofe_discrete
unit_ofe_mixin
limit_preserving_extIris.LimitPreserving.ext
prodOFIris.instOFunctorProdOF
prodOF_contractiveIris.instOFunctorContractiveProdOF
prodO_mapIris.Prod.mapO
proj1_sig_neIris.OFE.instNonExpansiveSubtypeVal
sig_discreteIris.OFE.instDiscreteSubtype
sig_ofe_mixinIris.OFE.instSubtype
▶proofmode_classes.v[src]0/9 (0%)
Rocq NameStatusDetails
IsOp
IsOp'
IsOp'LR
is_op_Some
is_op_lr_op
is_op_op
is_op_pair
is_op_pair_core_id_l
is_op_pair_core_id_r
▶reservation_map.v[src]0/44 (0%)
Rocq NameStatusDetails
ReservationMap_discrete
ReservationMap_ne
ReservationMap_proper
reservation_map
reservation_mapO
reservation_mapR
reservation_mapUR
reservation_map_alloc
reservation_map_cmra_discrete
reservation_map_cmra_mixin
reservation_map_data
reservation_map_data_core_id
reservation_map_data_discrete
reservation_map_data_is_op
reservation_map_data_mono
reservation_map_data_ne
reservation_map_data_op
reservation_map_data_proj_ne
reservation_map_data_proj_proper
reservation_map_data_proj_validN
reservation_map_data_proper
reservation_map_data_valid
reservation_map_dist
reservation_map_empty_instance
reservation_map_equiv
reservation_map_included
reservation_map_ofe_discrete
reservation_map_ofe_mixin
reservation_map_op_instance
reservation_map_pcore_instance
reservation_map_token
reservation_map_token_difference
reservation_map_token_discrete
reservation_map_token_proj_validN
reservation_map_token_union
reservation_map_token_valid
reservation_map_token_valid_op
reservation_map_ucmra_mixin
reservation_map_update
reservation_map_updateP
reservation_map_validN_eq
reservation_map_validN_instance
reservation_map_valid_eq
reservation_map_valid_instance
▶stepindex.v[src]0/51 (0%)
Rocq NameStatusDetails
SIdx.case
SIdx.eq_dec
SIdx.inhabited
SIdx.le_0_l
SIdx.le_0_r
SIdx.le_dec
SIdx.le_gt_cases
SIdx.le_lt_trans
SIdx.le_lteq
SIdx.le_neq
SIdx.le_ngt
SIdx.le_po
SIdx.le_succ_diag_r
SIdx.le_succ_l
SIdx.le_succ_l_2
SIdx.le_total
SIdx.limit
SIdx.limit_0
SIdx.limit_S
SIdx.limit_finite
SIdx.limit_lt_0
SIdx.lt_dec
SIdx.lt_ge_cases
SIdx.lt_le_incl
SIdx.lt_le_trans
SIdx.lt_nge
SIdx.lt_strict
SIdx.lt_succ_diag_r
SIdx.lt_succ_diag_r'
SIdx.lt_succ_r
SIdx.lt_trans
SIdx.lt_trichotomy
SIdx.lt_wf
SIdx.neq_0_lt_0
SIdx.neq_succ_0
SIdx.nlt_0_r
SIdx.nlt_succ_r
SIdx.rec
SIdx.rec_lim
SIdx.rec_lim_ext
SIdx.rec_succ
SIdx.rec_unfold
SIdx.rec_zero
SIdx.succ_inj
SIdx.succ_le_mono
SIdx.succ_lt_mono
SIdx.succ_neq
SIdx.weak_case
SIdxFinite
SIdxMixin
sidx
▶stepindex_finite.v[src]1/14 (7%)
Rocq NameStatusDetails
cmra_validN_S
cofe_finite
contractive_S
conv_compl_S
dist_S
dist_later_S
dist_later_fin
dist_later_fin_iff
dist_le
natSI
nat_sidx_finite
nat_sidx_mixin
ofe_mixin_finite
cmra_includedN_SIris.CMRA.incN_of_incN_succ
▶sts.v[src]0/101 (0%)
Rocq NameStatusDetails
auth_proper
frag_proper
sts.car
sts.closed
sts.closed_op
sts.closed_proper
sts.closed_proper'
sts.closed_steps
sts.closed_up
sts.closed_up_empty
sts.closed_up_set
sts.closed_up_set_empty
sts.elem_of_up
sts.elem_of_up_set
sts.frame_step
sts.frame_step_mono
sts.frame_step_proper
sts.step
sts.step_closed
sts.steps_closed
sts.stsT
sts.subseteq_up_set
sts.up
sts.up_closed
sts.up_op
sts.up_preserving
sts.up_proper
sts.up_set
sts.up_set_preserving
sts.up_set_proper
sts.up_set_subseteq
sts.up_subseteq
sts.up_up_set
sts_auth
sts_auth_frag_op
sts_auth_frag_up_op
sts_auth_frag_valid_inv
sts_auth_proper
sts_auth_valid
sts_car_core_disjoint_l
sts_car_core_idemp
sts_car_core_instance
sts_car_core_l
sts_car_core_mono
sts_car_core_proper
sts_car_core_valid
sts_car_disjoint_instance
sts_car_disjoint_ll
sts_car_disjoint_lr
sts_car_disjoint_move_l
sts_car_disjoint_move_r
sts_car_disjoint_proper
sts_car_disjoint_proper'
sts_car_disjoint_rl
sts_car_disjoint_symmetric
sts_car_equiv
sts_car_equivalence
sts_car_op_assoc
sts_car_op_comm
sts_car_op_proper
sts_car_op_valid
sts_car_valid_instance
sts_car_valid_proper
sts_car_valid_proper'
sts_equiv
sts_equivalence
sts_frag
sts_frag_core_id
sts_frag_op
sts_frag_proper
sts_frag_up
sts_frag_up_proper
sts_frag_up_valid
sts_frag_valid
sts_notok.frame_prim_step
sts_notok.mk_closed
sts_notok.prim_frame_step
sts_notok.stsT
sts_notok.stsT_tok
sts_notok.stsT_token
sts_notok.sts_notok
sts_notok.sts_step
sts_notok.sts_steps
sts_notok_update_auth
sts_op_instance
sts_res
sts_resO
sts_resR
sts_res_cmra_total
sts_res_disrete_cmra
sts_res_op_instance
sts_res_pcore_instance
sts_res_ra_mixin
sts_res_valid_instance
sts_up_set_intersection
sts_update_auth
sts_update_frag
sts_update_frag_up
to_sts_res
to_sts_res_op
to_sts_res_proper
▶ufrac.v[src]0/14 (0%)
Rocq NameStatusDetails
is_op_ufrac
ufrac
ufracO
ufracR
ufrac_cancelable
ufrac_cmra_discrete
ufrac_id_free
ufrac_included
ufrac_included_weak
ufrac_op
ufrac_op_instance
ufrac_pcore_instance
ufrac_ra_mixin
ufrac_valid_instance
▶updates.v[src]0/40 (0%)
Rocq NameStatusDetails
cmra_discrete_total_update
cmra_discrete_total_updateP
cmra_discrete_update
cmra_discrete_updateP
cmra_total_update
cmra_total_updateP
cmra_transport_updateP
cmra_transport_updateP'
cmra_update
cmra_updateP
cmra_updateP_compose
cmra_updateP_compose_l
cmra_updateP_id
cmra_updateP_op
cmra_updateP_op'
cmra_updateP_proper
cmra_updateP_weaken
cmra_update_exclusive
cmra_update_flip_proper_update
cmra_update_included
cmra_update_lift_updateP
cmra_update_op
cmra_update_op_flip_proper
cmra_update_op_l
cmra_update_op_proper
cmra_update_op_r
cmra_update_preorder
cmra_update_proper
cmra_update_proper_update
cmra_update_rewrite_relation
cmra_update_updateP
cmra_update_valid0
iso_cmra_updateP
iso_cmra_updateP'
option_update
option_updateP
option_updateP'
prod_update
prod_updateP
prod_updateP'
▶vector.v[src]0/21 (0%)
Rocq NameStatusDetails
list_cofe
vcons_discrete
vcons_ne
vcons_proper
vecO
vecOF
vecOF_contractive
vecO_map
vecO_map_ne
vec_dist
vec_equiv
vec_map
vec_map_ext_ne
vec_map_ne
vec_ofe_discrete
vec_ofe_mixin
vec_to_list_ne
vec_to_list_proper
vlookup_ne
vlookup_proper
vnil_discrete
▶view.v[src]0/108 (0%)
Rocq NameStatusDetails
ViewRelDiscrete
View_discrete
View_ne
View_proper
big_opL_view_frag
big_opMS_view_frag
big_opM_view_frag
big_opS_view_frag
view
viewO
viewO_map
viewO_map_ne
viewR
viewUR
view_auth
view_auth_core_id
view_auth_dfrac_included
view_auth_dfrac_includedN
view_auth_dfrac_is_op
view_auth_dfrac_op
view_auth_dfrac_op_inv
view_auth_dfrac_op_invN
view_auth_dfrac_op_inv_L
view_auth_dfrac_op_valid
view_auth_dfrac_op_validN
view_auth_dfrac_valid
view_auth_dfrac_validN
view_auth_discrete
view_auth_dist_inj
view_auth_included
view_auth_includedN
view_auth_inj
view_auth_ne
view_auth_op_valid
view_auth_op_validN
view_auth_proj_ne
view_auth_proj_proper
view_auth_proper
view_auth_valid
view_auth_validN
view_both_core_discarded
view_both_core_frac
view_both_core_id
view_both_dfrac_included
view_both_dfrac_includedN
view_both_dfrac_valid
view_both_dfrac_validN
view_both_included
view_both_includedN
view_both_valid
view_both_validN
view_cmra_discrete
view_cmra_mixin
view_core_eq
view_dist
view_empty_instance
view_equiv
view_frag
view_frag_core
view_frag_core_id
view_frag_discrete
view_frag_dist_inj
view_frag_included
view_frag_includedN
view_frag_inj
view_frag_is_op
view_frag_mono
view_frag_ne
view_frag_op
view_frag_proj_ne
view_frag_proj_proper
view_frag_proper
view_frag_sep_homomorphism
view_frag_valid
view_frag_validN
view_local_update
view_map
view_map_cmra_morphism
view_map_compose
view_map_ext
view_map_id
view_map_ne
view_ofe_discrete
view_ofe_mixin
view_op_eq
view_op_instance
view_pcore_eq
view_pcore_instance
view_rel
view_rel_ne
view_rel_proper
view_ucmra_mixin
view_update
view_updateP
view_updateP_auth_dfrac
view_updateP_auth_unpersist
view_updateP_both_unpersist
view_updateP_frag
view_update_alloc
view_update_auth
view_update_auth_persist
view_update_dealloc
view_update_dfrac_alloc
view_update_frag
view_validN_eq
view_validN_instance
view_valid_eq
view_valid_instance
▶base_logic/146/895 (16%)
▶bi.v[src]11/43 (26%)
Rocq NameStatusDetails
pure_elim'
pure_intro
pure_ne
uPred.ownM_ne
uPred.ownM_op
uPred.ownM_valid
uPred.uPred_and_unseal
uPred.uPred_bupd_unseal
uPred.uPred_emp_unseal
uPred.uPred_exist_unseal
uPred.uPred_forall_unseal
uPred.uPred_impl_unseal
uPred.uPred_later_unseal
uPred.uPred_or_unseal
uPred.uPred_persistently_unseal
uPred.uPred_pure_unseal
uPred.uPred_sep_unseal
uPred.uPred_si_emp_valid_unseal
uPred.uPred_si_pure_unseal
uPred.uPred_unseal
uPred.uPred_wand_unseal
uPredI
uPred_bi_later_mixin
uPred_bi_mixin
uPred_bi_persistently_mixin
uPred_bupd_mixin
uPred_emp
uPred_pure
uPred_pure_forall
uPred_sbi
uPred_sbi_mixin
uPred_sbi_prop_ext_mixin
uPred.bupd_ownM_updatePUPred.bupd_ownM_updateP
uPred.later_ownMUPred.later_ownM
uPred.ownM_forallUPred.ownM_forall
uPred.ownM_unitUPred.ownM_unit
uPred.persistently_ownM_coreUPred.persistently_ownM_core
uPred_affineUPred.instBIAffineUPred
uPred_bi_bupdUPred.instBIUpdateUPred
uPred_bi_bupd_sbiUPred.instBIBUpdateSbiUPred
uPred_later_contractiveUPred.instBILaterContractiveUPred
uPred_persistently_forallUPred.instBIPersistentlyForallUPred
uPred_sbi_emp_valid_existUPred.instSbiEmpValidExistUPred
▶bupd_alt.v[src]0/14 (0%)
Rocq NameStatusDetails
bupd_alt
bupd_alt_bupd
bupd_alt_bupd_iff
bupd_alt_flip_mono'
bupd_alt_frame_r
bupd_alt_intro
bupd_alt_mono
bupd_alt_mono'
bupd_alt_ne
bupd_alt_plainly
bupd_alt_proper
bupd_alt_trans
bupd_bupd_alt
ownM_updateP
▶derived.v[src]8/15 (53%)
Rocq NameStatusDetails
uPred.consistency
uPred.denote_modalities
uPred.denote_modality
uPred.modal_soundness
uPred.modality
uPred.ownM_proper
uPred.uPred_ownM_sep_homomorphism
uPred.bupd_ownM_updateUPred.bupd_ownM_update
uPred.bupd_soundnessUPred.bupd_soundness
uPred.intuitionistically_ownMUPred.intuitionistically_ownM
uPred.ownM_invalidUPred.ownM_invalid
uPred.ownM_monoUPred.ownM_mono
uPred.ownM_persistentUPred.ownM_persistent
uPred.ownM_timelessUPred.ownM_timeless
uPred.ownM_unit'UPred.ownM_unit'
▶lib/boxes.v[src]0/34 (0%)
Rocq NameStatusDetails
box
boxG
box_alloc
box_contractive
box_empty
box_fill
box_inv_ne
box_ne
box_own_agree
box_own_auth
box_own_auth_agree
box_own_auth_update
box_own_prop
box_own_prop_contractive
box_own_prop_ne
box_proper
boxΣ
slice
slice_combine
slice_contractive
slice_delete_empty
slice_delete_full
slice_empty
slice_fill
slice_iff
slice_insert_empty
slice_insert_full
slice_inv
slice_name
slice_ne
slice_persistent
slice_proper
slice_split
subG_boxΣ
▶lib/cancelable_invariants.v[src]0/29 (0%)
Rocq NameStatusDetails
cinv
cinvG
cinv_acc
cinv_acc_1
cinv_acc_strong
cinv_alloc
cinv_alloc_cofinite
cinv_alloc_open
cinv_alloc_strong
cinv_alloc_strong_open
cinv_cancel
cinv_contractive
cinv_excl
cinv_excl_excl
cinv_iff
cinv_ne
cinv_own
cinv_own_1_l
cinv_own_as_fractional
cinv_own_excl_alloc
cinv_own_fractional
cinv_own_timeless
cinv_own_valid
cinv_persistent
cinv_proper
cinvΣ
into_acc_cinv
into_inv_cinv
subG_cinvΣ
▶lib/fancy_updates.v[src]14/26 (54%)
Rocq NameStatusDetails
fupd_soundness_no_lc_unfold
has_lc
invGS_gen
invGpreS
invΣ
subG_invΣ
tac_lc_add_laterN_split
uPred_fupd
uPred_fupd_aux
uPred_fupd_def
uPred_fupd_mixin
uPred_fupd_unseal
fupd_soundness_genIris.fupd_soundness_gen
fupd_soundness_lcIris.fupd_soundness_lc
fupd_soundness_no_lcIris.fupd_soundness_no_lc
lc_fupd_add_laterIris.lc_fupd_add_later
lc_fupd_add_laterNIris.lc_fupd_add_laterN
lc_fupd_elim_laterIris.lc_fupd_elim_later
step_fupdN_soundness_genIris.step_fupdN_soundness_gen
step_fupdN_soundness_lcIris.step_fupdN_soundness_lc
step_fupdN_soundness_lc'Iris.step_fupdN_soundness_lc'
step_fupdN_soundness_no_lcIris.step_fupdN_soundness_no_lc
step_fupdN_soundness_no_lc'Iris.step_fupdN_soundness_no_lc'
uPred_bi_bupd_fupdIris.instBIUpdateFUpdateIProp
uPred_bi_fupdIris.uPred_bi_fupd
uPred_bi_fupd_sbi_no_lcIris.uPred_bi_fupd_plainly_no_lc
▶lib/fancy_updates_from_vs.v[src]0/1 (0%)
Rocq NameStatusDetails
fupd
▶lib/gen_heap.v[src]0/54 (0%)
Rocq NameStatusDetails
combine_sep_gives_meta_meta_token_1
combine_sep_gives_meta_meta_token_2
frame_pointsto
gen_heapGS
gen_heapGpreS
gen_heap_alloc
gen_heap_alloc_big
gen_heap_init
gen_heap_init_names
gen_heap_interp
gen_heap_update
gen_heap_valid
gen_heapΣ
meta
meta_agree
meta_aux
meta_def
meta_meta_token_valid
meta_meta_token_valid'
meta_persistent
meta_set
meta_timeless
meta_token
meta_token_aux
meta_token_combine_as
meta_token_def
meta_token_difference
meta_token_ne
meta_token_timeless
meta_token_union
meta_token_union_1
meta_token_union_2
meta_token_unseal
meta_token_valid_2
meta_unseal
pointsto
pointsto_agree
pointsto_as_fractional
pointsto_aux
pointsto_combine
pointsto_combine_as
pointsto_combine_sep_gives
pointsto_def
pointsto_frac_ne
pointsto_fractional
pointsto_ne
pointsto_persist
pointsto_persistent
pointsto_timeless
pointsto_unpersist
pointsto_unseal
pointsto_valid
pointsto_valid_2
subG_gen_heapGpreS
▶lib/gen_inv_heap.v[src]0/31 (0%)
Rocq NameStatusDetails
inv_heapGS
inv_heapGpreS
inv_heapN
inv_heap_init
inv_heap_inv
inv_heap_inv_P
inv_heap_inv_persistent
inv_heap_mapUR
inv_heapΣ
inv_pointsto
inv_pointsto_acc
inv_pointsto_lookup_Some
inv_pointsto_own
inv_pointsto_own_acc
inv_pointsto_own_acc_strong
inv_pointsto_own_inv
inv_pointsto_own_lookup_Some
inv_pointsto_own_proper
inv_pointsto_own_timeless
inv_pointsto_persistent
inv_pointsto_proper
inv_pointsto_timeless
lookup_to_inv_heap_None
lookup_to_inv_heap_Some
lookup_to_inv_heap_Some_2
make_inv_pointsto
subG_inv_heapGpreS
to_inv_heap
to_inv_heap_insert
to_inv_heap_singleton
to_inv_heap_valid
▶lib/ghost_map.v[src]0/48 (0%)
Rocq NameStatusDetails
ghost_mapG
ghost_map_alloc
ghost_map_alloc_empty
ghost_map_alloc_strong
ghost_map_alloc_strong_empty
ghost_map_auth
ghost_map_auth_agree
ghost_map_auth_as_fractional
ghost_map_auth_aux
ghost_map_auth_def
ghost_map_auth_fractional
ghost_map_auth_timeless
ghost_map_auth_unseal
ghost_map_auth_valid
ghost_map_auth_valid_2
ghost_map_delete
ghost_map_delete_big
ghost_map_elem
ghost_map_elem_agree
ghost_map_elem_as_fractional
ghost_map_elem_aux
ghost_map_elem_combine
ghost_map_elem_combine_as
ghost_map_elem_combine_gives
ghost_map_elem_def
ghost_map_elem_frac_ne
ghost_map_elem_fractional
ghost_map_elem_ne
ghost_map_elem_persist
ghost_map_elem_persistent
ghost_map_elem_timeless
ghost_map_elem_unpersist
ghost_map_elem_unseal
ghost_map_elem_valid
ghost_map_elem_valid_2
ghost_map_elems_unseal
ghost_map_insert
ghost_map_insert_big
ghost_map_insert_persist
ghost_map_insert_persist_big
ghost_map_lookup
ghost_map_lookup_big
ghost_map_lookup_combine_gives_1
ghost_map_lookup_combine_gives_2
ghost_map_update
ghost_map_update_big
ghost_mapΣ
subG_ghost_mapΣ
▶lib/ghost_var.v[src]0/24 (0%)
Rocq NameStatusDetails
frame_ghost_var
ghost_var
ghost_varG
ghost_var_agree
ghost_var_alloc
ghost_var_alloc_strong
ghost_var_as_fractional
ghost_var_aux
ghost_var_combine_as
ghost_var_combine_gives
ghost_var_def
ghost_var_fractional
ghost_var_persist
ghost_var_persistent
ghost_var_split
ghost_var_timeless
ghost_var_unpersist
ghost_var_unseal
ghost_var_update
ghost_var_update_2
ghost_var_update_halves
ghost_var_valid_2
ghost_varΣ
subG_ghost_varΣ
▶lib/gset_bij.v[src]0/27 (0%)
Rocq NameStatusDetails
gset_bijG
gset_bij_elem_of
gset_bij_own_alloc
gset_bij_own_alloc_empty
gset_bij_own_auth
gset_bij_own_auth_agree
gset_bij_own_auth_as_fractional
gset_bij_own_auth_aux
gset_bij_own_auth_def
gset_bij_own_auth_eq
gset_bij_own_auth_exclusive
gset_bij_own_auth_fractional
gset_bij_own_auth_timeless
gset_bij_own_elem
gset_bij_own_elem_agree
gset_bij_own_elem_aux
gset_bij_own_elem_def
gset_bij_own_elem_eq
gset_bij_own_elem_get
gset_bij_own_elem_get_big
gset_bij_own_elem_persistent
gset_bij_own_elem_timeless
gset_bij_own_extend
gset_bij_own_extend_internal
gset_bij_own_valid
gset_bijΣ
subG_gset_bijΣ
▶lib/invariants.v[src]21/30 (70%)
Rocq NameStatusDetails
fresh_inv_name
into_acc_inv
into_inv_inv
inv
inv_aux
inv_def
inv_proper
inv_unseal
own_inv
except_0_invIris.except_0_inv
inv_accIris.inv_acc
inv_acc_strongIris.inv_acc_strong
inv_acc_timelessIris.inv_acc_timeless
inv_allocIris.inv_alloc
inv_alloc_openIris.inv_alloc_open
inv_alterIris.inv_alter
inv_combineIris.inv_combine
inv_combine_dup_lIris.inv_combine_dup_l
inv_contractiveIris.inv_contractive
inv_iffIris.inv_iff
inv_neIris.inv_ne
inv_persistentIris.inv_persistent
inv_splitIris.inv_split
inv_split_lIris.inv_split_l
inv_split_rIris.inv_split_r
is_except_0_invIris.is_except_0_inv
own_inv_accIris.own_inv_acc
own_inv_allocIris.own_inv_alloc
own_inv_alloc_openIris.own_inv_alloc_open
own_inv_to_invIris.own_inv_to_inv
▶lib/iprop.v[src]0/24 (0%)
Rocq NameStatusDetails
Export.iPrePropO
Export.iPreProp_cofe
Export.iProp_fold
Export.iProp_fold_unfold
Export.iProp_result
Export.iProp_unfold
Export.iProp_unfold_equivI
Export.iProp_unfold_fold
Export.iResUR
gFunctor
gFunctors
gFunctors.app
gFunctors.nil
gFunctors.singleton
gid
gname
gnameO
iResF
iResUR
subG
subG_app_l
subG_app_r
subG_inv
subG_refl
▶lib/later_credits.v[src]52/79 (66%)
Rocq NameStatusDetails
combine_sep_lc_S_l
combine_sep_lc_add
lc
lcGS
lcGpreS
lc_aux
lc_def
lc_split
lc_supply
lc_supply_aux
lc_supply_def
lc_supply_unseal
lc_unseal
lcΣ
le_upd.bi_bupd_mixin_le_upd
le_upd.frame_le_upd
le_upd.le_upd_aux
le_upd.le_upd_def
le_upd.le_upd_equiv_proper
le_upd.le_upd_flip_mono'
le_upd.le_upd_mono'
le_upd.le_upd_unseal
le_upd_if.frame_le_upd_if
le_upd_if.le_upd_if_flip_mono'
le_upd_if.le_upd_if_mono
le_upd_if.le_upd_if_proper
subG_lcΣ
from_sep_lc_SIris.instFromSepIPropLcSuccOfNatCredit
from_sep_lc_addIris.instFromSepIPropLcHAddCredit
into_sep_lc_SIris.instIntoSepIPropLcSuccOfNatCredit
into_sep_lc_addIris.instIntoSepIPropLcHAddCredit
lc_0_persistentIris.instPersistentIPropLcOfNatCredit
lc_decrease_supplyIris.lc_decrease_supply
lc_succIris.lc_succ
lc_supply_boundIris.lc_supply_bound
lc_timelessIris.instTimelessIPropLc
lc_weakenIris.lc_weaken
lc_zeroIris.lc_zero
le_upd.bupd_le_updIris.bupd_le_upd
le_upd.elim_bupd_le_updIris.instElimModalIPropTrueFalseBupdLe_upd
le_upd.elim_modal_le_updIris.instElimModalIPropTrueFalseLe_upd
le_upd.except_0_le_updIris.except_0_le_upd
le_upd.from_assumption_le_updIris.from_assumption_le_upd
le_upd.from_modal_le_updIris.instFromModalIPropTrueModality_idLe_upd
le_upd.from_pure_le_updIris.instFromPureIPropLe_upd
le_upd.is_except_0_le_updIris.instIsExcept0IPropLe_upd
le_upd.lc_allocIris.lc_alloc
le_upd.lc_soundnessIris.lc_soundness
le_upd.le_updIris.le_upd
le_upd.le_upd_bindIris.le_upd_bind
le_upd.le_upd_elimIris.le_upd_elim
le_upd.le_upd_elim_completeIris.le_upd_elim_complete
le_upd.le_upd_frame_lIris.le_upd_frame_l
le_upd.le_upd_frame_rIris.le_upd_frame_r
le_upd.le_upd_introIris.le_upd_intro
le_upd.le_upd_laterIris.le_upd_later
le_upd.le_upd_later_elimIris.le_upd_later_elim
le_upd.le_upd_monoIris.le_upd_mono
le_upd.le_upd_neIris.instNonExpansiveIPropLe_upd
le_upd.le_upd_preIris.le_upd_pre
le_upd.le_upd_pre_contractiveIris.instContractiveForallIPropLe_upd_pre
le_upd.le_upd_transIris.le_upd_trans
le_upd.le_upd_unfoldIris.le_upd_unfold
le_upd_if.bupd_le_upd_ifIris.bupd_le_upd_if
le_upd_if.elim_bupd_le_upd_ifIris.instElimModalIPropTrueFalseBupdLe_upd_if
le_upd_if.elim_modal_le_upd_ifIris.instElimModalIPropTrueFalseLe_upd_if
le_upd_if.except_0_le_upd_ifIris.except_0_le_upd_if
le_upd_if.from_assumption_le_upd_ifIris.from_assumption_le_upd_if
le_upd_if.from_modal_le_upd_ifIris.instFromModalIPropTrueModality_idLe_upd_if
le_upd_if.from_pure_le_upd_ifIris.instFromPureIPropLe_upd_if
le_upd_if.is_except_0_le_upd_ifIris.instIsExcept0IPropLe_upd_if
le_upd_if.le_upd_ifIris.le_upd_if
le_upd_if.le_upd_if_bindIris.le_upd_if_bind
le_upd_if.le_upd_if_frame_lIris.le_upd_if_frame_l
le_upd_if.le_upd_if_frame_rIris.le_upd_if_frame_r
le_upd_if.le_upd_if_introIris.le_upd_if_intro
le_upd_if.le_upd_if_mono'Iris.le_upd_if_mono
le_upd_if.le_upd_if_neIris.le_upd_if_ne
le_upd_if.le_upd_if_transIris.le_upd_if_trans
▶lib/mono_Z.v[src]0/26 (0%)
Rocq NameStatusDetails
mono_ZG
mono_Z_auth_own
mono_Z_auth_own_agree
mono_Z_auth_own_as_fractional
mono_Z_auth_own_aux
mono_Z_auth_own_def
mono_Z_auth_own_exclusive
mono_Z_auth_own_fractional
mono_Z_auth_own_persistent
mono_Z_auth_own_timeless
mono_Z_auth_own_unseal
mono_Z_lb_own
mono_Z_lb_own_0
mono_Z_lb_own_aux
mono_Z_lb_own_def
mono_Z_lb_own_get
mono_Z_lb_own_le
mono_Z_lb_own_persistent
mono_Z_lb_own_timeless
mono_Z_lb_own_unseal
mono_Z_lb_own_valid
mono_Z_own_alloc
mono_Z_own_persist
mono_Z_own_unpersist
mono_Z_own_update
mono_ZΣ
▶lib/mono_nat.v[src]0/28 (0%)
Rocq NameStatusDetails
mono_natG
mono_nat_auth_own
mono_nat_auth_own_agree
mono_nat_auth_own_as_fractional
mono_nat_auth_own_aux
mono_nat_auth_own_def
mono_nat_auth_own_exclusive
mono_nat_auth_own_fractional
mono_nat_auth_own_persistent
mono_nat_auth_own_timeless
mono_nat_auth_own_unseal
mono_nat_lb_own
mono_nat_lb_own_0
mono_nat_lb_own_aux
mono_nat_lb_own_def
mono_nat_lb_own_get
mono_nat_lb_own_le
mono_nat_lb_own_persistent
mono_nat_lb_own_timeless
mono_nat_lb_own_unseal
mono_nat_lb_own_valid
mono_nat_own_alloc
mono_nat_own_alloc_strong
mono_nat_own_persist
mono_nat_own_unpersist
mono_nat_own_update
mono_natΣ
subG_mono_natΣ
▶lib/na_invariants.v[src]0/22 (0%)
Rocq NameStatusDetails
into_acc_na
into_inv_na
na_alloc
na_inv
na_invG
na_inv_acc
na_inv_alloc
na_inv_contractive
na_inv_iff
na_inv_ne
na_inv_persistent
na_inv_pool_name
na_inv_proper
na_invΣ
na_own
na_own_acc
na_own_disjoint
na_own_empty
na_own_empty_persistent
na_own_timeless
na_own_union
subG_na_invG
▶lib/own.v[src]27/72 (38%)
Rocq NameStatusDetails
big_opL_own
big_opL_own_1
big_opMS_own
big_opMS_own_1
big_opM_own
big_opM_own_1
big_opS_own
big_opS_own_1
combine_sep_as_own
combine_sep_gives_own
from_and_own_persistent
from_sep_own
iRes_project
iRes_project_above
iRes_project_below
iRes_project_ne
iRes_project_op
iRes_project_singleton
iRes_singleton_validI
inG
inG_fold
inG_fold_unfold
inG_unfold
inG_unfold_fold
inG_unfold_validN
into_and_own
into_sep_own
later_internal_eq_iRes_singleton
later_own
own_and
own_and_discrete_total
own_and_discrete_total_False
own_and_total
own_aux
own_cmra_sep_entails_homomorphism
own_cmra_sep_homomorphism
own_def
own_eq
own_forall
own_forall_pred
own_forall_pred_total
own_forall_total
own_mono'
own_proper
subG_inG
iRes_singletonIris.iSingleton
iRes_singleton_core_idIris.instCoreIdIResURISingletonOfApIProp
iRes_singleton_discreteIris.iSingleton_discreteE
iRes_singleton_neIris.instNonExpansiveApIPropIResURISingleton
iRes_singleton_opIris.iSingleton_op
ownIris.iOwn
own_allocIris.iOwn_alloc
own_alloc_cofiniteIris.iOwn_alloc_cofinite
own_alloc_cofinite_depIris.iOwn_alloc_cofinite_dep
own_alloc_depIris.iOwn_alloc_dep
own_alloc_strongIris.iOwn_alloc_strong
own_alloc_strong_depIris.iOwn_alloc_strong_dep
own_core_persistentIris.instPersistentIPropIOwnOfCoreIdAp
own_monoIris.iOwn_mono
own_neIris.iOwn_ne
own_opIris.iOwn_op
own_timelessIris.iOwn_timeless
own_unitIris.iOwn_unit
own_updateIris.iOwn_update
own_updatePIris.iOwn_updateP
own_update_2Iris.iOwn_update_op
own_update_3Iris.iOwn_update_op_op
own_validIris.iOwn_cmraValid
own_valid_2Iris.iOwn_cmraValid_op
own_valid_3Iris.iOwn_cmraValid_op_op
own_valid_lIris.iOwn_valid_l
own_valid_rIris.iOwn_valid_r
▶lib/proph_map.v[src]0/19 (0%)
Rocq NameStatusDetails
proph
proph_aux
proph_def
proph_exclusive
proph_list_resolves
proph_mapGS
proph_mapGpreS
proph_map_agree
proph_map_init
proph_map_interp
proph_map_new_proph
proph_map_resolve_proph
proph_mapΣ
proph_resolves_in_list
proph_timeless
proph_unseal
proph_val_list
resolves_insert
subG_proph_mapGpreS
▶lib/saved_prop.v[src]0/54 (0%)
Rocq NameStatusDetails
savedAnythingG
savedAnythingΣ
saved_anything_agree
saved_anything_alloc
saved_anything_alloc_cofinite
saved_anything_alloc_strong
saved_anything_as_fractional
saved_anything_combine_as
saved_anything_combine_gives
saved_anything_discarded_persistent
saved_anything_fractional
saved_anything_ne
saved_anything_own
saved_anything_persist
saved_anything_proper
saved_anything_unpersist
saved_anything_update
saved_anything_update_2
saved_anything_update_halves
saved_anything_valid
saved_anything_valid_2
saved_pred_agree
saved_pred_alloc
saved_pred_alloc_cofinite
saved_pred_alloc_strong
saved_pred_as_fractional
saved_pred_discarded_persistent
saved_pred_fractional
saved_pred_own
saved_pred_own_contractive
saved_pred_persist
saved_pred_unpersist
saved_pred_update
saved_pred_update_2
saved_pred_update_halves
saved_pred_valid
saved_pred_valid_2
saved_prop_agree
saved_prop_alloc
saved_prop_alloc_cofinite
saved_prop_alloc_strong
saved_prop_as_fractional
saved_prop_discarded_persistent
saved_prop_fractional
saved_prop_own
saved_prop_own_contractive
saved_prop_persist
saved_prop_unpersist
saved_prop_update
saved_prop_update_2
saved_prop_update_halves
saved_prop_valid
saved_prop_valid_2
subG_savedAnythingΣ
▶lib/token.v[src]5/11 (45%)
Rocq NameStatusDetails
subG_tokenΣ
token_aux
token_combine_gives
token_def
token_unseal
tokenΣ
tokenGIris.TokenG
token_allocIris.token_alloc
token_alloc_strongIris.token_alloc_strong
token_exclusiveIris.token_exclusive
token_timelessIris.token_timeless
▶lib/wsat.v[src]0/28 (0%)
Rocq NameStatusDetails
invariant_lookup
invariant_unfold
invariant_unfold_contractive
ownD
ownD_disjoint
ownD_empty
ownD_op
ownD_op'
ownD_singleton_twice
ownE
ownE_disjoint
ownE_empty
ownE_op
ownE_op'
ownE_singleton_twice
ownI
ownI_alloc
ownI_alloc_open
ownI_close
ownI_contractive
ownI_open
ownI_persistent
wsat
wsatGS.subG_wsatΣ
wsatGS.wsatGS
wsatGS.wsatGpreS
wsatGS.wsatΣ
wsat_alloc
▶proofmode.v[src]0/6 (0%)
Rocq NameStatusDetails
combine_sep_as_ownM
combine_sep_gives_ownM
from_sep_ownM
from_sep_ownM_core_id
into_and_ownM
into_sep_ownM
▶upred.v[src]8/150 (5%)
Rocq NameStatusDetails
uPred
uPredO
uPredOF
uPredOF_contractive
uPredO_map
uPredO_map_ne
uPred_alt
uPred_and
uPred_and_aux
uPred_and_def
uPred_and_unseal
uPred_bupd
uPred_bupd_aux
uPred_bupd_def
uPred_bupd_unseal
uPred_cofe
uPred_compl
uPred_dist
uPred_dist'
uPred_entails
uPred_equiv
uPred_equiv'
uPred_exist
uPred_exist_aux
uPred_exist_def
uPred_exist_unseal
uPred_forall
uPred_forall_aux
uPred_forall_def
uPred_forall_unseal
uPred_holds_ne
uPred_impl
uPred_impl_aux
uPred_impl_def
uPred_impl_unseal
uPred_later
uPred_later_aux
uPred_later_def
uPred_later_unseal
uPred_map
uPred_map_compose
uPred_map_ext
uPred_map_id
uPred_map_ne
uPred_ne
uPred_ofe_mixin
uPred_or
uPred_or_aux
uPred_or_def
uPred_or_unseal
uPred_ownM
uPred_ownM_aux
uPred_ownM_def
uPred_ownM_unseal
uPred_persistently
uPred_persistently_aux
uPred_persistently_def
uPred_persistently_unseal
uPred_primitive.True_sep_1
uPred_primitive.True_sep_2
uPred_primitive.and_elim_l
uPred_primitive.and_elim_r
uPred_primitive.and_intro
uPred_primitive.and_ne
uPred_primitive.bupd_frame_r
uPred_primitive.bupd_intro
uPred_primitive.bupd_mono
uPred_primitive.bupd_ownM_updateP
uPred_primitive.bupd_trans
uPred_primitive.entails_anti_sym
uPred_primitive.entails_lim
uPred_primitive.entails_po
uPred_primitive.equiv_entails
uPred_primitive.exist_elim
uPred_primitive.exist_intro
uPred_primitive.exist_ne
uPred_primitive.forall_elim
uPred_primitive.forall_intro
uPred_primitive.forall_ne
uPred_primitive.impl_elim_l'
uPred_primitive.impl_intro_r
uPred_primitive.impl_ne
uPred_primitive.later_exist_false
uPred_primitive.later_false_em
uPred_primitive.later_forall_2
uPred_primitive.later_intro
uPred_primitive.later_mono
uPred_primitive.later_ownM
uPred_primitive.later_persistently_1
uPred_primitive.later_persistently_2
uPred_primitive.later_sep_1
uPred_primitive.later_sep_2
uPred_primitive.or_elim
uPred_primitive.or_intro_l
uPred_primitive.or_intro_r
uPred_primitive.or_ne
uPred_primitive.ownM_forall
uPred_primitive.ownM_unit
uPred_primitive.persistently_and_sep_l_1
uPred_primitive.persistently_elim
uPred_primitive.persistently_exist_1
uPred_primitive.persistently_forall_2
uPred_primitive.persistently_idemp_2
uPred_primitive.persistently_impl_si_pure
uPred_primitive.persistently_mono
uPred_primitive.persistently_ownM_core
uPred_primitive.prop_ext_2
uPred_primitive.sep_assoc'
uPred_primitive.sep_comm'
uPred_primitive.sep_mono
uPred_primitive.sep_ne
uPred_primitive.si_emp_valid_later_1
uPred_primitive.si_emp_valid_mono
uPred_primitive.si_emp_valid_ne
uPred_primitive.si_emp_valid_si_pure
uPred_primitive.si_pure_forall_2
uPred_primitive.si_pure_impl_2
uPred_primitive.si_pure_later
uPred_primitive.si_pure_mono
uPred_primitive.si_pure_ne
uPred_primitive.si_pure_si_emp_valid
uPred_primitive.uPred_unseal
uPred_primitive.wand_elim_l'
uPred_primitive.wand_intro_r
uPred_primitive.wand_ne
uPred_proper
uPred_sep
uPred_sep_aux
uPred_sep_def
uPred_sep_unseal
uPred_si_emp_valid
uPred_si_emp_valid_aux
uPred_si_emp_valid_def
uPred_si_emp_valid_unseal
uPred_si_pure
uPred_si_pure_aux
uPred_si_pure_def
uPred_si_pure_unseal
uPred_wand
uPred_wand_aux
uPred_wand_def
uPred_wand_unseal
uPred_primitive.bupd_neUPred.bupd_ne
uPred_primitive.bupd_si_pureUPred.bupd_si_pure
uPred_primitive.later_contractiveUPred.later_contractive
uPred_primitive.ownM_neUPred.ownM_ne
uPred_primitive.ownM_opUPred.ownM_op
uPred_primitive.ownM_validUPred.ownM_valid
uPred_primitive.persistently_neUPred.persistently_ne
uPred_primitive.si_emp_valid_exist_1Iris.siEmpValid_exist_mp
▶bi/623/2257 (28%)
▶algebra.v[src]18/56 (32%)
Rocq NameStatusDetails
Some_included_totalI
cmra_later_opI
cmra_morphism_validI
cmra_validI_op_l
cmra_validI_op_r
csum_includedI
csum_validI
dfrac_agree_validI
dfrac_agree_validI_2
discrete_fun_validI
excl_auth_agreeI
excl_includedI
excl_validI
f_homom_includedI
frac_agree_validI
frac_agree_validI_2
gmap_equivI
gmap_union_equiv_eqI
gmap_validI
id_freeI_l
id_freeI_r
list_equivI
option_includedI
option_included_totalI
option_validI
prod_includedI
prod_validI
singleton_validI
ucmra_unit_validI
view_auth_dfrac_validI
view_auth_validI
view_both_dfrac_validI
view_both_dfrac_validI_1
view_both_dfrac_validI_2
view_both_validI
view_both_validI_1
view_both_validI_2
view_frag_validI
agree_equivIIris.agree_equivI
agree_includedIIris.agree_includedI
agree_op_equiv_to_agreeIIris.agree_op_equiv_toAgreeI
agree_op_invIIris.agree_op_invI
auth_auth_dfrac_op_validIIris.auth_dfrac_op_validI
auth_auth_dfrac_validIIris.auth_dfrac_validI
auth_auth_validIIris.auth_validI
auth_both_dfrac_validIIris.both_dfrac_validI
auth_both_validIIris.auth_both_validI
auth_frag_validIIris.frag_validI
gmap_view_both_dfrac_validIIris.auth_op_frag_validI
gmap_view_both_validIIris.auth_op_frag_one_validI
gmap_view_both_validI_totalIris.auth_op_frag_validI_total
gmap_view_frag_op_validIIris.frag_op_frag_validI
to_agree_includedIIris.toAgree_includedI
to_agree_op_validIIris.toAgree_op_validI
to_agree_uninjIIris.toAgree_uninjI
to_agree_validIIris.toAgree_validI
▶big_op.v[src]345/482 (72%)
Rocq NameStatusDetails
big_andL_zip_seqZ
big_andM_kmap
big_andM_map_seq
big_andM_map_seqZ
big_orL_zip_seqZ
big_sepL2
big_sepL2_mono'
big_sepL2_ne'
big_sepL2_proper'
big_sepL_mono'
big_sepL_sepM
big_sepL_sepMS
big_sepL_sepS
big_sepL_zip_seqZ
big_sepM2
big_sepM2_affine
big_sepM2_affine'
big_sepM2_affinely_pure_2
big_sepM2_alt
big_sepM2_alt_lookup
big_sepM2_and
big_sepM2_aux
big_sepM2_closed
big_sepM2_def
big_sepM2_delete
big_sepM2_delete_l
big_sepM2_delete_r
big_sepM2_dom
big_sepM2_empty
big_sepM2_empty'
big_sepM2_empty_affine
big_sepM2_empty_l
big_sepM2_empty_persistent
big_sepM2_empty_r
big_sepM2_empty_timeless
big_sepM2_flip
big_sepM2_flip_mono'
big_sepM2_fmap
big_sepM2_fmap_l
big_sepM2_fmap_r
big_sepM2_forall
big_sepM2_fst_snd
big_sepM2_impl
big_sepM2_insert
big_sepM2_insert_2
big_sepM2_insert_acc
big_sepM2_insert_delete
big_sepM2_intro
big_sepM2_laterN_2
big_sepM2_later_1
big_sepM2_later_2
big_sepM2_lookup
big_sepM2_lookup_acc
big_sepM2_lookup_acc_impl
big_sepM2_lookup_iff
big_sepM2_lookup_l
big_sepM2_lookup_r
big_sepM2_mono
big_sepM2_mono'
big_sepM2_ne
big_sepM2_ne'
big_sepM2_ne_2
big_sepM2_persistent
big_sepM2_persistent'
big_sepM2_persistently
big_sepM2_proper
big_sepM2_proper'
big_sepM2_proper_2
big_sepM2_pure
big_sepM2_pure_1
big_sepM2_sep
big_sepM2_sepM
big_sepM2_sepM_2
big_sepM2_sep_2
big_sepM2_singleton
big_sepM2_timeless
big_sepM2_timeless'
big_sepM2_union_inv_l
big_sepM2_union_inv_r
big_sepM2_unseal
big_sepM2_wand
big_sepMS_affine
big_sepMS_affine'
big_sepMS_affinely_pure_2
big_sepMS_and
big_sepMS_delete
big_sepMS_disj_union
big_sepMS_dup
big_sepMS_elem_of
big_sepMS_elem_of_acc
big_sepMS_elem_of_acc_impl
big_sepMS_empty
big_sepMS_empty'
big_sepMS_empty_affine
big_sepMS_empty_persistent
big_sepMS_empty_timeless
big_sepMS_flip_mono'
big_sepMS_forall
big_sepMS_impl
big_sepMS_insert
big_sepMS_intro
big_sepMS_later
big_sepMS_laterN
big_sepMS_laterN_2
big_sepMS_later_2
big_sepMS_mono
big_sepMS_mono'
big_sepMS_ne
big_sepMS_persistent
big_sepMS_persistent'
big_sepMS_persistently
big_sepMS_proper
big_sepMS_pure
big_sepMS_pure_1
big_sepMS_sep
big_sepMS_sepL
big_sepMS_sepM
big_sepMS_sepMS
big_sepMS_sepS
big_sepMS_sep_2
big_sepMS_singleton
big_sepMS_subseteq
big_sepMS_timeless
big_sepMS_timeless'
big_sepMS_wand
big_sepM_gset_to_gmap
big_sepM_kmap
big_sepM_map_seq
big_sepM_map_seqZ
big_sepM_sepL
big_sepM_sepM
big_sepM_sepM2_diag
big_sepM_sepMS
big_sepM_sepS
big_sepS_affine'
big_sepS_persistent'
big_sepS_sepMS
big_andL_absorbingIris.BI.BigAndL.bigAndL_absorbing
big_andL_absorbing'Iris.BI.BigAndL.bigAndL_absorbing_inst
big_andL_andIris.BI.BigAndL.bigAndL_and_equiv
big_andL_appIris.BI.BigAndL.bigAndL_append
big_andL_bindIris.BI.BigAndL.bigAndL_flatMap
big_andL_consIris.BI.BigAndL.bigAndL_cons
big_andL_elem_ofIris.BI.BigAndL.bigAndL_mem
big_andL_fmapIris.BI.BigAndL.bigAndL_map
big_andL_forallIris.BI.BigAndL.bigAndL_forall
big_andL_id_mono'Iris.BI.BigAndL.bigAndL_id_mono_of_forall
big_andL_implIris.BI.BigAndL.bigAndL_impl
big_andL_introIris.BI.BigAndL.bigAndL_intro
big_andL_laterIris.BI.BigAndL.bigAndL_later
big_andL_laterNIris.BI.BigAndL.bigAndL_laterN
big_andL_lookupIris.BI.BigAndL.bigAndL_lookup
big_andL_monoIris.BI.BigAndL.bigAndL_mono
big_andL_mono'Iris.BI.BigAndL.bigAndL_mono_of_forall
big_andL_neIris.BI.BigAndL.bigAndL_dist
big_andL_nilIris.BI.BigAndL.bigAndL_nil
big_andL_nil'Iris.BI.BigAndL.bigAndL_nil_intro
big_andL_nil_absorbingIris.BI.BigAndL.bigAndL_nil_absorbing_inst
big_andL_nil_persistentIris.BI.BigAndL.bigAndL_nil_persistent_inst
big_andL_nil_timelessIris.BI.BigAndL.bigAndL_nil_timeless_inst
big_andL_persistentIris.BI.BigAndL.bigAndL_persistent
big_andL_persistent'Iris.BI.BigAndL.bigAndL_persistent_inst
big_andL_persistentlyIris.BI.BigAndL.bigAndL_persistently
big_andL_properIris.BI.BigAndL.bigAndL_equiv
big_andL_pureIris.BI.BigAndL.bigAndL_pure
big_andL_pure_1Iris.BI.BigAndL.bigAndL_pure_intro
big_andL_pure_2Iris.BI.BigAndL.bigAndL_pure_elim
big_andL_singletonIris.BI.BigAndL.bigAndL_singleton
big_andL_snocIris.BI.BigAndL.bigAndL_snoc
big_andL_submseteqIris.BI.BigAndL.bigAndL_submseteq
big_andL_timelessIris.BI.BigAndL.bigAndL_timeless
big_andL_timeless'Iris.BI.BigAndL.bigAndL_timeless_inst
big_andL_zip_seqIris.BI.BigAndL.bigAndL_zip_seq
big_andM_andIris.BI.BigAndM.bigAndM_and_equiv
big_andM_deleteIris.BI.BigAndM.bigAndM_delete
big_andM_emptyIris.BI.BigAndM.bigAndM_empty
big_andM_empty'Iris.BI.BigAndM.bigAndM_empty_intro
big_andM_empty_persistentIris.BI.BigAndM.bigAndM_nil_persistent_inst
big_andM_empty_timelessIris.BI.BigAndM.bigAndM_nil_timeless_inst
big_andM_filterIris.BI.BigAndM.bigAndM_filter
big_andM_filter'Iris.BI.BigAndM.bigAndM_filter_cond
big_andM_fmapIris.BI.BigAndM.bigAndM_map
big_andM_fn_insertIris.BI.BigAndM.bigAndM_fn_insert
big_andM_fn_insert'Iris.BI.BigAndM.bigAndM_fn_insert_cond
big_andM_forallIris.BI.BigAndM.bigAndM_forall
big_andM_implIris.BI.BigAndM.bigAndM_impl
big_andM_insertIris.BI.BigAndM.bigAndM_insert
big_andM_insert_2Iris.BI.BigAndM.bigAndM_insert_elim
big_andM_insert_deleteIris.BI.BigAndM.bigAndM_insert_delete
big_andM_introIris.BI.BigAndM.bigAndM_intro
big_andM_laterIris.BI.BigAndM.bigAndM_later
big_andM_laterNIris.BI.BigAndM.bigAndM_laterN
big_andM_lookupIris.BI.BigAndM.bigAndM_lookup
big_andM_lookup_domIris.BI.BigAndM.bigAndM_lookup_dom
big_andM_monoIris.BI.BigAndM.bigAndM_mono
big_andM_mono'Iris.BI.BigAndM.bigAndM_mono_of_forall
big_andM_neIris.BI.BigAndM.bigAndM_dist
big_andM_omapIris.BI.BigAndM.bigAndM_filterMap
big_andM_persistentIris.BI.BigAndM.bigAndM_persistent
big_andM_persistent'Iris.BI.BigAndM.bigAndM_persistent_inst
big_andM_persistentlyIris.BI.BigAndM.bigAndM_persistently
big_andM_properIris.BI.BigAndM.bigAndM_equiv
big_andM_pureIris.BI.BigAndM.bigAndM_pure
big_andM_pure_1Iris.BI.BigAndM.bigAndM_pure_intro
big_andM_pure_2Iris.BI.BigAndM.bigAndM_pure_elim
big_andM_singletonIris.BI.BigAndM.bigAndM_singleton
big_andM_subseteqIris.BI.BigAndM.bigAndM_subseteq
big_andM_timelessIris.BI.BigAndM.bigAndM_timeless
big_andM_timeless'Iris.BI.BigAndM.bigAndM_timeless_inst
big_andM_unionIris.BI.BigAndM.bigAndM_union
big_orL_appIris.BI.BigOrL.bigOrL_append
big_orL_bindIris.BI.BigOrL.bigOrL_flatMap
big_orL_consIris.BI.BigOrL.bigOrL_cons
big_orL_elem_ofIris.BI.BigOrL.bigOrL_mem
big_orL_existIris.BI.BigOrL.bigOrL_exist
big_orL_fmapIris.BI.BigOrL.bigOrL_map
big_orL_id_mono'Iris.BI.BigOrL.bigOrL_id_mono_of_forall
big_orL_introIris.BI.BigOrL.bigOrL_intro
big_orL_laterIris.BI.BigOrL.bigOrL_later
big_orL_laterNIris.BI.BigOrL.bigOrL_laterN
big_orL_monoIris.BI.BigOrL.bigOrL_mono
big_orL_mono'Iris.BI.BigOrL.bigOrL_mono_of_forall
big_orL_neIris.BI.BigOrL.bigOrL_dist
big_orL_nilIris.BI.BigOrL.bigOrL_nil
big_orL_nil_persistentIris.BI.BigOrL.bigOrL_nil_persistent
big_orL_nil_timelessIris.BI.BigOrL.bigOrL_nil_timeless
big_orL_orIris.BI.BigOrL.bigOrL_or_equiv
big_orL_persistentIris.BI.BigOrL.bigOrL_persistent
big_orL_persistent'Iris.BI.BigOrL.bigOrL_persistent_inst
big_orL_persistentlyIris.BI.BigOrL.bigOrL_persistently
big_orL_properIris.BI.BigOrL.bigOrL_equiv
big_orL_pureIris.BI.BigOrL.bigOrL_pure
big_orL_sep_lIris.BI.BigOrL.bigOrL_sep_left
big_orL_sep_rIris.BI.BigOrL.bigOrL_sep_right
big_orL_singletonIris.BI.BigOrL.bigOrL_singleton
big_orL_snocIris.BI.BigOrL.bigOrL_snoc
big_orL_submseteqIris.BI.BigOrL.bigOrL_submseteq
big_orL_timelessIris.BI.BigOrL.bigOrL_timeless
big_orL_timeless'Iris.BI.BigOrL.bigOrL_timeless_inst
big_orL_zip_seqIris.BI.BigOrL.bigOrL_zip_seq
big_sepL2_affineIris.BI.BigSepL2.bigSepL2_affine
big_sepL2_affine'Iris.BI.BigSepL2.bigSepL2_affine_inst
big_sepL2_affinely_pure_2Iris.BI.BigSepL2.bigSepL2_affinely_pure_elim
big_sepL2_altIris.BI.BigSepL2.bigSepL2_alt
big_sepL2_andIris.BI.BigSepL2.bigSepL2_and
big_sepL2_appIris.BI.BigSepL2.bigSepL2_app_wand
big_sepL2_app_invIris.BI.BigSepL2.bigSepL2_append
big_sepL2_app_inv_lIris.BI.BigSepL2.bigSepL2_app_inv_left
big_sepL2_app_inv_rIris.BI.BigSepL2.bigSepL2_app_inv_right
big_sepL2_app_same_lengthIris.BI.BigSepL2.bigSepL2_app_same_length
big_sepL2_closedIris.BI.BigSepL2.bigSepL2_closed
big_sepL2_consIris.BI.BigSepL2.bigSepL2_cons
big_sepL2_cons_inv_lIris.BI.BigSepL2.bigSepL2_cons_inv_left
big_sepL2_cons_inv_rIris.BI.BigSepL2.bigSepL2_cons_inv_right
big_sepL2_const_sepL_lIris.BI.BigSepL2.bigSepL2_const_sepL_left
big_sepL2_const_sepL_rIris.BI.BigSepL2.bigSepL2_const_sepL_right
big_sepL2_deleteIris.BI.BigSepL2.bigSepL2_delete_cond
big_sepL2_delete'Iris.BI.BigSepL2.bigSepL2_delete
big_sepL2_flipIris.BI.BigSepL2.bigSepL2_flip
big_sepL2_flip_mono'Iris.BI.BigSepL2.bigSepL2_mono_of_forall
big_sepL2_fmap_lIris.BI.BigSepL2.bigSepL2_map_left
big_sepL2_fmap_rIris.BI.BigSepL2.bigSepL2_map_right
big_sepL2_forallIris.BI.BigSepL2.bigSepL2_forall
big_sepL2_fst_sndIris.BI.BigSepL2.bigSepL2_fst_snd
big_sepL2_implIris.BI.BigSepL2.bigSepL2_impl
big_sepL2_insert_accIris.BI.BigSepL2.bigSepL2_insert_acc
big_sepL2_introIris.BI.BigSepL2.bigSepL2_intro
big_sepL2_laterN_2Iris.BI.BigSepL2.bigSepL2_laterN_2
big_sepL2_later_1Iris.BI.BigSepL2.bigSepL2_later_1
big_sepL2_later_2Iris.BI.BigSepL2.bigSepL2_later_2
big_sepL2_lengthIris.BI.BigSepL2.bigSepL2_length
big_sepL2_lookupIris.BI.BigSepL2.bigSepL2_lookup
big_sepL2_lookup_accIris.BI.BigSepL2.bigSepL2_lookup_acc
big_sepL2_lookup_acc_implIris.BI.BigSepL2.bigSepL2_lookup_acc_impl
big_sepL2_lookup_lIris.BI.BigSepL2.bigSepL2_lookup_left
big_sepL2_lookup_rIris.BI.BigSepL2.bigSepL2_lookup_right
big_sepL2_monoIris.BI.BigSepL2.bigSepL2_mono
big_sepL2_neIris.BI.BigSepL2.bigSepL2_dist
big_sepL2_ne_2Iris.BI.BigSepL2.bigSepL2_dist_2
big_sepL2_nilIris.BI.BigSepL2.bigSepL2_nil
big_sepL2_nil'Iris.BI.BigSepL2.bigSepL2_nil_affine
big_sepL2_nil_affineIris.BI.BigSepL2.bigSepL2_nil_affine_inst
big_sepL2_nil_inv_lIris.BI.BigSepL2.bigSepL2_nil_inv_left
big_sepL2_nil_inv_rIris.BI.BigSepL2.bigSepL2_nil_inv_right
big_sepL2_nil_persistentIris.BI.BigSepL2.bigSepL2_nil_persistent_inst
big_sepL2_nil_timelessIris.BI.BigSepL2.bigSepL2_nil_timeless
big_sepL2_persistentIris.BI.BigSepL2.bigSepL2_persistent
big_sepL2_persistent'Iris.BI.BigSepL2.bigSepL2_persistent_inst
big_sepL2_persistentlyIris.BI.BigSepL2.bigSepL2_persistently
big_sepL2_properIris.BI.BigSepL2.bigSepL2_equiv
big_sepL2_proper_2Iris.BI.BigSepL2.bigSepL2_proper_2
big_sepL2_pureIris.BI.BigSepL2.bigSepL2_pure
big_sepL2_pure_1Iris.BI.BigSepL2.bigSepL2_pure_intro
big_sepL2_replicate_lIris.BI.BigSepL2.bigSepL2_replicate_left
big_sepL2_replicate_rIris.BI.BigSepL2.bigSepL2_replicate_right
big_sepL2_reverseIris.BI.BigSepL2.bigSepL2_reverse
big_sepL2_reverse_2Iris.BI.BigSepL2.bigSepL2_reverse_2
big_sepL2_sepIris.BI.BigSepL2.bigSepL2_sep_equiv
big_sepL2_sepLIris.BI.BigSepL2.bigSepL2_sepL
big_sepL2_sepL_2Iris.BI.BigSepL2.bigSepL2_sepL_2
big_sepL2_sep_2Iris.BI.BigSepL2.bigSepL2_sep_equiv_symm
big_sepL2_sep_sepL_lIris.BI.BigSepL2.bigSepL2_sep_sepL_left
big_sepL2_sep_sepL_rIris.BI.BigSepL2.bigSepL2_sep_sepL_right
big_sepL2_singletonIris.BI.BigSepL2.bigSepL2_singleton
big_sepL2_snocIris.BI.BigSepL2.bigSepL2_snoc
big_sepL2_timelessIris.BI.BigSepL2.bigSepL2_timeless
big_sepL2_timeless'Iris.BI.BigSepL2.bigSepL2_timeless'
big_sepL2_wandIris.BI.BigSepL2.bigSepL2_wand
big_sepL_affineIris.BI.BigSepL.bigSepL_affine
big_sepL_affine'Iris.BI.BigSepL.bigSepL_affine_inst
big_sepL_affine_idIris.BI.BigSepL.bigSepL_affine_id
big_sepL_affinely_pure_2Iris.BI.BigSepL.bigSepL_affinely_pure_elim
big_sepL_andIris.BI.BigSepL.bigSepL_and
big_sepL_appIris.BI.BigSepL.bigSepL_append
big_sepL_bindIris.BI.BigSepL.bigSepL_flatMap
big_sepL_consIris.BI.BigSepL.bigSepL_cons
big_sepL_deleteIris.BI.BigSepL.bigSepL_delete_cond
big_sepL_delete'Iris.BI.BigSepL.bigSepL_delete
big_sepL_dupIris.BI.BigSepL.bigSepL_dup
big_sepL_elem_ofIris.BI.BigSepL.bigSepL_mem
big_sepL_elem_of_accIris.BI.BigSepL.bigSepL_mem_acc
big_sepL_empIris.BI.BigSepL.bigSepL_emp
big_sepL_flip_mono'Iris.BI.BigSepL.bigSepL_flip_mono
big_sepL_fmapIris.BI.BigSepL.bigSepL_map
big_sepL_forallIris.BI.BigSepL.bigSepL_forall_equiv
big_sepL_id_mono'Iris.BI.BigSepL.bigSepL_id_mono
big_sepL_implIris.BI.BigSepL.bigSepL_impl
big_sepL_insert_accIris.BI.BigSepL.bigSepL_insert_acc
big_sepL_introIris.BI.BigSepL.bigSepL_intro
big_sepL_laterIris.BI.BigSepL.bigSepL_later
big_sepL_laterNIris.BI.BigSepL.bigSepL_laterN
big_sepL_laterN_2Iris.BI.BigSepL.bigSepL_laterN_2
big_sepL_later_2Iris.BI.BigSepL.bigSepL_later_2
big_sepL_lookupIris.BI.BigSepL.bigSepL_lookup
big_sepL_lookup_accIris.BI.BigSepL.bigSepL_lookup_acc
big_sepL_lookup_acc_implIris.BI.BigSepL.bigSepL_lookup_acc_impl
big_sepL_monoIris.BI.BigSepL.bigSepL_mono
big_sepL_neIris.BI.BigSepL.bigSepL_dist
big_sepL_nilIris.BI.BigSepL.bigSepL_nil
big_sepL_nil'Iris.BI.BigSepL.bigSepL_nil_intro
big_sepL_nil_affineIris.BI.BigSepL.bigSepL_nil_affine_inst
big_sepL_nil_persistentIris.BI.BigSepL.bigSepL_nil_persistent
big_sepL_nil_timelessIris.BI.BigSepL.bigSepL_nil_timeless_inst
big_sepL_omapIris.BI.BigSepL.bigSepL_filterMap
big_sepL_persistentIris.BI.BigSepL.bigSepL_persistent
big_sepL_persistent'Iris.BI.BigSepL.bigSepL_persistent_inst
big_sepL_persistent_idIris.BI.BigSepL.bigSepL_persistent_id
big_sepL_persistentlyIris.BI.BigSepL.bigSepL_persistently
big_sepL_properIris.BI.BigSepL.bigSepL_equiv
big_sepL_pureIris.BI.BigSepL.bigSepL_pure
big_sepL_pure_1Iris.BI.BigSepL.bigSepL_pure_intro
big_sepL_replicateIris.BI.BigSepL.bigSepL_replicate
big_sepL_sepIris.BI.BigSepL.bigSepL_sep_equiv
big_sepL_sepLIris.BI.BigSepL.bigSepL_comm
big_sepL_sepL2_diagIris.BI.BigSepL2.bigSepL_sepL2_diag
big_sepL_sep_2Iris.BI.BigSepL.bigSepL_sep_equiv_symm
big_sepL_sep_zipIris.BI.BigSepL.bigSepL_sep_zip
big_sepL_sep_zip_withIris.BI.BigSepL.bigSepL_sep_zip_with
big_sepL_singletonIris.BI.BigSepL.bigSepL_singleton
big_sepL_snocIris.BI.BigSepL.bigSepL_snoc
big_sepL_submseteqIris.BI.BigSepL.bigSepL_submseteq
big_sepL_take_dropIris.BI.BigSepL.bigSepL_take_drop
big_sepL_timelessIris.BI.BigSepL.bigSepL_timeless
big_sepL_timeless'Iris.BI.BigSepL.bigSepL_timeless_inst
big_sepL_timeless_idIris.BI.BigSepL.bigSepL_timeless_id
big_sepL_wandIris.BI.BigSepL.bigSepL_wand
big_sepL_zip_seqIris.BI.BigSepL.bigSepL_zip_seq
big_sepL_zip_withIris.BI.BigSepL.bigSepL_zip_with
big_sepM_affineIris.BI.BigSepM.bigSepM_affine
big_sepM_affine'Iris.BI.BigSepM.bigSepM_affine_inst
big_sepM_affinely_pure_2Iris.BI.BigSepM.bigSepM_affinely_pure_elim
big_sepM_andIris.BI.BigSepM.bigSepM_and
big_sepM_deleteIris.BI.BigSepM.bigSepM_delete
big_sepM_domIris.BI.BigSepM.bigSepM_dom
big_sepM_dupIris.BI.BigSepM.bigSepM_dup
big_sepM_emptyIris.BI.BigSepM.bigSepM_empty
big_sepM_empty'Iris.BI.BigSepM.bigSepM_empty_intro
big_sepM_empty_affineIris.BI.BigSepM.bigSepM_nil_affine_inst
big_sepM_empty_persistentIris.BI.BigSepM.bigSepM_nil_persistent_inst
big_sepM_empty_timelessIris.BI.BigSepM.bigSepM_nil_timeless_inst
big_sepM_filterIris.BI.BigSepM.bigSepM_filter
big_sepM_filter'Iris.BI.BigSepM.bigSepM_filter_cond
big_sepM_flip_mono'Iris.BI.BigSepM.bigSepM_flip_mono
big_sepM_fmapIris.BI.BigSepM.bigSepM_map
big_sepM_fn_insertIris.BI.BigSepM.bigSepM_fn_insert
big_sepM_fn_insert'Iris.BI.BigSepM.bigSepM_fn_insert_key
big_sepM_forallIris.BI.BigSepM.bigSepM_forall
big_sepM_implIris.BI.BigSepM.bigSepM_impl
big_sepM_impl_dom_subseteqIris.BI.BigSepM.bigSepM_impl_dom_subseteq
big_sepM_impl_strongIris.BI.BigSepM.bigSepM_impl_strong
big_sepM_insertIris.BI.BigSepM.bigSepM_insert
big_sepM_insert_2Iris.BI.BigSepM.bigSepM_insert_elim
big_sepM_insert_accIris.BI.BigSepM.bigSepM_insert_acc
big_sepM_insert_deleteIris.BI.BigSepM.bigSepM_insert_delete
big_sepM_insert_overrideIris.BI.BigSepM.bigSepM_insert_exist
big_sepM_insert_override_1Iris.BI.BigSepM.bigSepM_insert_exist_elim
big_sepM_insert_override_2Iris.BI.BigSepM.bigSepM_insert_exist_intro
big_sepM_introIris.BI.BigSepM.bigSepM_intro
big_sepM_laterIris.BI.BigSepM.bigSepM_later
big_sepM_laterNIris.BI.BigSepM.bigSepM_laterN
big_sepM_laterN_2Iris.BI.BigSepM.bigSepM_laterN_2
big_sepM_later_2Iris.BI.BigSepM.bigSepM_later_2
big_sepM_list_to_mapIris.BI.BigSepM.bigSepM_ofList
big_sepM_lookupIris.BI.BigSepM.bigSepM_lookup
big_sepM_lookup_accIris.BI.BigSepM.bigSepM_lookup_acc
big_sepM_lookup_acc_implIris.BI.BigSepM.bigSepM_lookup_acc_impl
big_sepM_lookup_domIris.BI.BigSepM.bigSepM_lookup_dom
big_sepM_map_to_listIris.BI.BigSepM.bigSepM_toList
big_sepM_monoIris.BI.BigSepM.bigSepM_mono
big_sepM_mono'Iris.BI.BigSepM.bigSepM_mono_of_forall
big_sepM_neIris.BI.BigSepM.bigSepM_dist
big_sepM_omapIris.BI.BigSepM.bigSepM_filterMap
big_sepM_persistentIris.BI.BigSepM.bigSepM_persistent
big_sepM_persistent'Iris.BI.BigSepM.bigSepM_persistent_inst
big_sepM_persistentlyIris.BI.BigSepM.bigSepM_persistently
big_sepM_properIris.BI.BigSepM.bigSepM_equiv
big_sepM_pureIris.BI.BigSepM.bigSepM_pure
big_sepM_pure_1Iris.BI.BigSepM.bigSepM_pure_intro
big_sepM_sepIris.BI.BigSepM.bigSepM_sep_equiv
big_sepM_sep_2Iris.BI.BigSepM.bigSepM_sep_equiv_symm
big_sepM_sep_zipIris.BI.BigSepM.bigSepM_sep_zip
big_sepM_sep_zip_withIris.BI.BigSepM.bigSepM_sep_zipWith
big_sepM_singletonIris.BI.BigSepM.bigSepM_singleton
big_sepM_subseteqIris.BI.BigSepM.bigSepM_subseteq
big_sepM_timelessIris.BI.BigSepM.bigSepM_timeless
big_sepM_timeless'Iris.BI.BigSepM.bigSepM_timeless_inst
big_sepM_unionIris.BI.BigSepM.bigSepM_union
big_sepM_wandIris.BI.BigSepM.bigSepM_wand
big_sepS_affineIris.BI.BigSepS.bigSepS_affine
big_sepS_affinely_pure_2Iris.BI.BigSepS.bigSepS_affinely_pure_elim
big_sepS_andIris.BI.BigSepS.bigSepS_and
big_sepS_deleteIris.BI.BigSepS.bigSepS_delete
big_sepS_delete_2Iris.BI.BigSepS.bigSepS_delete_elim
big_sepS_dupIris.BI.BigSepS.bigSepS_dup
big_sepS_elem_ofIris.BI.BigSepS.bigSepS_elem_of
big_sepS_elem_of_accIris.BI.BigSepS.bigSepS_elem_of_acc
big_sepS_elem_of_acc_implIris.BI.BigSepS.bigSepS_elem_of_acc_impl
big_sepS_elementsIris.BI.BigSepS.bigSepS_elements
big_sepS_empIris.BI.BigSepS.bigSepS_emp
big_sepS_emptyIris.BI.BigSepS.bigSepS_empty
big_sepS_empty'Iris.BI.BigSepS.bigSepS_empty_intro
big_sepS_empty_affineIris.BI.BigSepS.bigSepS_empty_affine_inst
big_sepS_empty_persistentIris.BI.BigSepS.bigSepS_empty_persistent_inst
big_sepS_empty_timelessIris.BI.BigSepS.bigSepS_empty_timeless_inst
big_sepS_filterIris.BI.BigSepS.bigSepS_filter
big_sepS_filter'Iris.BI.BigSepS.bigSepS_filter_cond
big_sepS_filter_accIris.BI.BigSepS.bigSepS_filter_acc
big_sepS_filter_acc'Iris.BI.BigSepS.bigSepS_filter_acc_cond
big_sepS_flip_mono'Iris.BI.BigSepS.bigSepS_flip_mono
big_sepS_fn_insertIris.BI.BigSepS.bigSepS_fn_insert
big_sepS_fn_insert'Iris.BI.BigSepS.bigSepS_fn_insert_key
big_sepS_forallIris.BI.BigSepS.bigSepS_forall
big_sepS_implIris.BI.BigSepS.bigSepS_impl
big_sepS_insertIris.BI.BigSepS.bigSepS_insert
big_sepS_insert_2Iris.BI.BigSepS.bigSepS_insert_elim
big_sepS_insert_2'Iris.BI.BigSepS.bigSepS_insert_elim_wand
big_sepS_introIris.BI.BigSepS.bigSepS_intro
big_sepS_laterIris.BI.BigSepS.bigSepS_later
big_sepS_laterNIris.BI.BigSepS.bigSepS_laterN
big_sepS_laterN_2Iris.BI.BigSepS.bigSepS_laterN_2
big_sepS_later_2Iris.BI.BigSepS.bigSepS_later_2
big_sepS_list_to_setIris.BI.BigSepS.bigSepS_of_list
big_sepS_monoIris.BI.BigSepS.bigSepS_mono
big_sepS_mono'Iris.BI.BigSepS.bigSepS_mono_of_forall
big_sepS_neIris.BI.BigSepS.bigSepS_ne
big_sepS_persistentIris.BI.BigSepS.bigSepS_persistent
big_sepS_persistentlyIris.BI.BigSepS.bigSepS_persistently
big_sepS_properIris.BI.BigSepS.bigSepS_proper
big_sepS_pureIris.BI.BigSepS.bigSepS_pure
big_sepS_pure_1Iris.BI.BigSepS.bigSepS_pure_intro
big_sepS_sepIris.BI.BigSepS.bigSepS_sep
big_sepS_sepLIris.BI.BigSepS.bigSepS_comm_list
big_sepS_sepMIris.BI.BigSepS.bigSepS_comm_map
big_sepS_sepSIris.BI.BigSepS.bigSepS_comm_set
big_sepS_sep_2Iris.BI.BigSepS.bigSepS_sep_symm
big_sepS_singletonIris.BI.BigSepS.bigSepS_singleton
big_sepS_subseteqIris.BI.BigSepS.bigSepS_subseteq
big_sepS_timelessIris.BI.BigSepS.bigSepS_timeless
big_sepS_timeless'Iris.BI.BigSepS.bigSepS_timeless_inst
big_sepS_unionIris.BI.BigSepS.bigSepS_union
big_sepS_union_2Iris.BI.BigSepS.bigSepS_union_elim
big_sepS_wandIris.BI.BigSepS.bigSepS_wand
▶cmra.v[src]28/31 (90%)
Rocq NameStatusDetails
internal_cmra_valid_proper
internal_cmra_valid_timeless
internal_included_proper
internal_cmra_validIris.internalCmraValid
internal_cmra_valid_absorbingIris.internalCmraValid_absorbing
internal_cmra_valid_discreteIris.internalCmraValid_discrete
internal_cmra_valid_elimIris.internalCmraValid_elim
internal_cmra_valid_entailsIris.internalCmraValid_entails
internal_cmra_valid_introIris.internalCmraValid_intro
internal_cmra_valid_neIris.internalCmraValid_ne
internal_cmra_valid_persistentIris.internalCmraValid_persistent
internal_cmra_valid_plainIris.internalCmraValid_plain
internal_cmra_valid_weakenIris.internalCmraValid_weaken
internal_includedIris.internalCmraIncluded
internal_included_absorbingIris.internalCmraIncluded_absorbing
internal_included_discreteIris.internalCmraIncluded_discrete
internal_included_introIris.internalCmraIncluded_intro
internal_included_nonexpansiveIris.internalCmraIncluded_ne
internal_included_persistentIris.internalCmraIncluded_persistent
internal_included_plainIris.internalCmraIncluded_plain
internal_included_reflIris.internalCmraIncluded_refl
internal_included_timelessIris.internalCmraIncluded_timeless
internal_included_transIris.internalCmraIncluded_trans
intuitionistically_internal_cmra_validIris.intuitionistically_internalCmraValid
intuitionistically_internal_includedIris.intuitionistically_internalCmraIncluded
persistently_internal_cmra_validIris.persistently_internalCmraValid
persistently_internal_includedIris.persistently_internalCmraIncluded
plainly_internal_cmra_validIris.plainly_internalCmraValid
plainly_internal_includedIris.plainly_internalCmraIncluded
si_pure_internal_cmra_validIris.siPure_internalCmraValid
si_pure_internal_includedIris.siPure_internalCmraIncluded
▶derived_connectives.v[src]0/16 (0%)
Rocq NameStatusDetails
Absorbing
Affine
Persistent
Timeless
bi_absorbingly
bi_absorbingly_if
bi_affinely
bi_affinely_if
bi_except_0
bi_iff
bi_intuitionistically
bi_intuitionistically_if
bi_laterN
bi_persistently_if
bi_wandM
bi_wand_iff
▶derived_laws.v[src]12/459 (3%)
Rocq NameStatusDetails
bi.Absorbing_proper
bi.Affine_proper
bi.False_affine
bi.False_and
bi.False_elim
bi.False_impl
bi.False_or
bi.False_sep
bi.False_wand
bi.Persistent_proper
bi.True_affine_all_affine
bi.True_and
bi.True_emp
bi.True_impl
bi.True_intro
bi.True_or
bi.True_sep
bi.True_sep'
bi.True_sep_2
bi.absorbing_absorbingly
bi.absorbingly_True
bi.absorbingly_absorbing
bi.absorbingly_and_1
bi.absorbingly_elim_persistently
bi.absorbingly_emp_True
bi.absorbingly_exist
bi.absorbingly_flip_mono'
bi.absorbingly_forall
bi.absorbingly_idemp
bi.absorbingly_if_absorbingly
bi.absorbingly_if_and_1
bi.absorbingly_if_exist
bi.absorbingly_if_flag_mono
bi.absorbingly_if_flip_mono'
bi.absorbingly_if_forall
bi.absorbingly_if_idemp
bi.absorbingly_if_intro
bi.absorbingly_if_mono
bi.absorbingly_if_mono'
bi.absorbingly_if_ne
bi.absorbingly_if_or
bi.absorbingly_if_persistent
bi.absorbingly_if_proper
bi.absorbingly_if_pure
bi.absorbingly_if_sep
bi.absorbingly_if_sep_l
bi.absorbingly_if_sep_lr
bi.absorbingly_if_sep_r
bi.absorbingly_if_wand
bi.absorbingly_intro
bi.absorbingly_intuitionistically_into_persistently
bi.absorbingly_mono
bi.absorbingly_mono'
bi.absorbingly_ne
bi.absorbingly_or
bi.absorbingly_persistent
bi.absorbingly_proper
bi.absorbingly_pure
bi.absorbingly_sep
bi.absorbingly_sep_l
bi.absorbingly_sep_lr
bi.absorbingly_sep_r
bi.absorbingly_wand
bi.affine_affinely
bi.affinely_False
bi.affinely_True_emp
bi.affinely_absorbingly_elim
bi.affinely_affine
bi.affinely_affinely_if
bi.affinely_and
bi.affinely_and_l
bi.affinely_and_lr
bi.affinely_and_r
bi.affinely_elim
bi.affinely_elim_emp
bi.affinely_emp
bi.affinely_exist
bi.affinely_flip_mono'
bi.affinely_forall
bi.affinely_idemp
bi.affinely_if_absorbingly_if_elim
bi.affinely_if_affine
bi.affinely_if_and
bi.affinely_if_and_l
bi.affinely_if_and_lr
bi.affinely_if_and_r
bi.affinely_if_elim
bi.affinely_if_emp
bi.affinely_if_exist
bi.affinely_if_flag_mono
bi.affinely_if_flip_mono'
bi.affinely_if_idemp
bi.affinely_if_intro'
bi.affinely_if_mono
bi.affinely_if_mono'
bi.affinely_if_ne
bi.affinely_if_or
bi.affinely_if_persistent
bi.affinely_if_proper
bi.affinely_if_sep
bi.affinely_if_sep_2
bi.affinely_intro
bi.affinely_intro'
bi.affinely_mono
bi.affinely_mono'
bi.affinely_ne
bi.affinely_or
bi.affinely_persistent
bi.affinely_proper
bi.affinely_sep
bi.affinely_sep_2
bi.and_False
bi.and_True
bi.and_absorbing
bi.and_affine_l
bi.and_affine_r
bi.and_alt
bi.and_assoc
bi.and_comm
bi.and_elim_l'
bi.and_elim_r'
bi.and_emp
bi.and_emp'
bi.and_exist_l
bi.and_exist_r
bi.and_flip_mono'
bi.and_idem
bi.and_mono
bi.and_mono'
bi.and_mono_l
bi.and_mono_r
bi.and_or_l
bi.and_or_r
bi.and_parallel
bi.and_persistent
bi.and_proper
bi.and_sep_intuitionistically
bi.and_sep_persistently
bi.bi_affine_absorbing
bi.bi_affine_positive
bi.bi_and_monoid
bi.bi_emp_valid_flip_mono
bi.bi_emp_valid_mono
bi.bi_emp_valid_proper
bi.bi_or_monoid
bi.bi_persistently_and_homomorphism
bi.bi_persistently_or_homomorphism
bi.bi_persistently_sep_entails_homomorphism
bi.bi_persistently_sep_entails_weak_homomorphism
bi.bi_persistently_sep_homomorphism
bi.bi_persistently_sep_weak_homomorphism
bi.bi_pure_forall_em
bi.bi_sep_monoid
bi.decide_bi_True
bi.decide_emp
bi.emp_absorbing_all_absorbing
bi.emp_affine
bi.emp_and
bi.emp_and'
bi.emp_or
bi.emp_persistent
bi.emp_sep
bi.emp_wand
bi.entails_anti_sym
bi.entails_eq_True
bi.entails_equiv_and
bi.entails_equiv_l
bi.entails_equiv_r
bi.entails_impl
bi.entails_impl_True
bi.entails_proper
bi.entails_wand
bi.entails_wand'
bi.equiv_entails_1_1
bi.equiv_entails_1_2
bi.equiv_entails_2
bi.equiv_iff
bi.equiv_wand_iff
bi.exist_absorbing
bi.exist_affine
bi.exist_exist
bi.exist_flip_mono'
bi.exist_forall
bi.exist_impl_forall
bi.exist_intro'
bi.exist_mono
bi.exist_mono'
bi.exist_persistent
bi.exist_proper
bi.exist_unit
bi.exist_wand_forall
bi.forall_absorbing
bi.forall_affine
bi.forall_elim'
bi.forall_flip_mono'
bi.forall_forall
bi.forall_mono
bi.forall_mono'
bi.forall_persistent
bi.forall_proper
bi.forall_unit
bi.from_option_persistent
bi.iff_equiv
bi.iff_ne
bi.iff_proper
bi.iff_refl
bi.iff_sym
bi.iff_trans
bi.impl_absorbing
bi.impl_alt
bi.impl_curry
bi.impl_elim
bi.impl_elim_r'
bi.impl_entails
bi.impl_flip_mono'
bi.impl_intro_l
bi.impl_mono
bi.impl_mono'
bi.impl_proper
bi.impl_refl
bi.impl_trans
bi.impl_wand
bi.impl_wand_1
bi.impl_wand_2
bi.impl_wand_intuitionistically
bi.impl_wand_persistently
bi.impl_wand_persistently_2
bi.intuitionistic
bi.intuitionistic_intuitionistically
bi.intuitionistically_False
bi.intuitionistically_True_emp
bi.intuitionistically_affine
bi.intuitionistically_affinely
bi.intuitionistically_affinely_elim
bi.intuitionistically_alt_fixpoint
bi.intuitionistically_and
bi.intuitionistically_def
bi.intuitionistically_elim
bi.intuitionistically_elim_emp
bi.intuitionistically_emp
bi.intuitionistically_exist
bi.intuitionistically_flip_mono'
bi.intuitionistically_forall
bi.intuitionistically_idemp
bi.intuitionistically_if_False
bi.intuitionistically_if_affine
bi.intuitionistically_if_and
bi.intuitionistically_if_elim
bi.intuitionistically_if_emp
bi.intuitionistically_if_exist
bi.intuitionistically_if_flag_mono
bi.intuitionistically_if_flip_mono'
bi.intuitionistically_if_idemp
bi.intuitionistically_if_intro'
bi.intuitionistically_if_mono
bi.intuitionistically_if_mono'
bi.intuitionistically_if_ne
bi.intuitionistically_if_or
bi.intuitionistically_if_proper
bi.intuitionistically_if_sep
bi.intuitionistically_if_sep_2
bi.intuitionistically_if_unfold
bi.intuitionistically_impl_wand_2
bi.intuitionistically_into_persistently
bi.intuitionistically_into_persistently_1
bi.intuitionistically_intro
bi.intuitionistically_intro'
bi.intuitionistically_intuitionistically_if
bi.intuitionistically_mono'
bi.intuitionistically_ne
bi.intuitionistically_or
bi.intuitionistically_persistent
bi.intuitionistically_persistently_elim
bi.intuitionistically_proper
bi.intuitionistically_sep
bi.intuitionistically_sep_2
bi.intuitionistically_sep_dup
bi.iter_modal_intro
bi.iter_modal_mono
bi.limit_preserving_Persistent
bi.limit_preserving_emp_valid
bi.or_False
bi.or_True
bi.or_absorbing
bi.or_affine
bi.or_alt
bi.or_and_l
bi.or_and_r
bi.or_assoc
bi.or_comm
bi.or_emp
bi.or_exist
bi.or_flip_mono'
bi.or_idem
bi.or_intro_l'
bi.or_intro_r'
bi.or_mono
bi.or_mono'
bi.or_mono_l
bi.or_mono_r
bi.or_persistent
bi.or_proper
bi.persistent_absorbingly_affinely
bi.persistent_absorbingly_affinely_2
bi.persistent_and_affinely_sep_l
bi.persistent_and_affinely_sep_l_1
bi.persistent_and_affinely_sep_r
bi.persistent_and_affinely_sep_r_1
bi.persistent_and_sep
bi.persistent_and_sep_1
bi.persistent_and_sep_assoc
bi.persistent_impl_wand_affinely
bi.persistent_persistently
bi.persistent_persistently_2
bi.persistent_sep_dup
bi.persistent_sep_dup_1
bi.persistently_True
bi.persistently_True_emp
bi.persistently_absorbing
bi.persistently_affinely_elim
bi.persistently_alt_fixpoint
bi.persistently_alt_fixpoint'
bi.persistently_and
bi.persistently_and_emp
bi.persistently_and_emp_elim
bi.persistently_and_intuitionistically_sep_l
bi.persistently_and_intuitionistically_sep_r
bi.persistently_and_sep
bi.persistently_and_sep_assoc
bi.persistently_and_sep_elim_emp
bi.persistently_and_sep_l
bi.persistently_and_sep_l_1
bi.persistently_and_sep_r
bi.persistently_and_sep_r_1
bi.persistently_elim
bi.persistently_emp
bi.persistently_emp_intro
bi.persistently_entails_l
bi.persistently_entails_r
bi.persistently_exist
bi.persistently_flip_mono'
bi.persistently_forall
bi.persistently_forall_1
bi.persistently_idemp
bi.persistently_idemp_1
bi.persistently_if_absorbing
bi.persistently_if_and
bi.persistently_if_exist
bi.persistently_if_flip_mono'
bi.persistently_if_idemp
bi.persistently_if_mono
bi.persistently_if_mono'
bi.persistently_if_ne
bi.persistently_if_or
bi.persistently_if_proper
bi.persistently_if_pure
bi.persistently_if_sep
bi.persistently_if_sep_2
bi.persistently_impl
bi.persistently_impl_wand
bi.persistently_impl_wand_2
bi.persistently_into_absorbingly
bi.persistently_intro
bi.persistently_intro'
bi.persistently_mono'
bi.persistently_or
bi.persistently_persistent
bi.persistently_proper
bi.persistently_pure
bi.persistently_sep
bi.persistently_sep_2
bi.persistently_sep_dup
bi.persistently_wand
bi.pure_False
bi.pure_True
bi.pure_absorbing
bi.pure_alt
bi.pure_and
bi.pure_elim
bi.pure_elim_l
bi.pure_elim_r
bi.pure_exist
bi.pure_flip_mono
bi.pure_iff
bi.pure_impl_forall
bi.pure_mono
bi.pure_mono'
bi.pure_or
bi.pure_persistent
bi.pure_proper
bi.pure_wand_forall
bi.sep_False
bi.sep_True
bi.sep_True'
bi.sep_True_2
bi.sep_absorbing_l
bi.sep_absorbing_r
bi.sep_affine
bi.sep_and
bi.sep_and_l
bi.sep_and_r
bi.sep_assoc
bi.sep_comm
bi.sep_elim_emp_valid_l
bi.sep_elim_emp_valid_r
bi.sep_elim_l
bi.sep_elim_r
bi.sep_emp
bi.sep_exist_l
bi.sep_exist_r
bi.sep_flip_mono'
bi.sep_forall_l
bi.sep_forall_r
bi.sep_intro_emp_valid_l
bi.sep_intro_emp_valid_r
bi.sep_mono'
bi.sep_mono_l
bi.sep_mono_r
bi.sep_or_l
bi.sep_or_r
bi.sep_persistent
bi.sep_proper
bi.wandM_sound
bi.wand_absorbing_l
bi.wand_absorbing_r
bi.wand_alt
bi.wand_apply
bi.wand_elim_l
bi.wand_elim_r
bi.wand_elim_r'
bi.wand_entails
bi.wand_entails'
bi.wand_flip_mono'
bi.wand_frame_l
bi.wand_frame_r
bi.wand_iff_equiv
bi.wand_iff_ne
bi.wand_iff_proper
bi.wand_iff_refl
bi.wand_iff_sym
bi.wand_iff_trans
bi.wand_intro_l
bi.wand_mono
bi.wand_mono'
bi.wand_proper
bi.wand_refl
bi.wand_trans
bi.True_emp_iff_BiAffineIris.BI.biaffine_iff_true_emp
bi.impl_elim_lIris.BI.imp_elim_l
bi.impl_elim_rIris.BI.imp_elim_r
bi.limit_preserving_entailsIris.BI.LimitPreserving.entails
bi.persistent_entails_lIris.BI.persistent_entails_r
bi.persistent_entails_rIris.BI.persistent_entails_l
bi.pure_forallIris.BI.pure_forall
bi.pure_forall_1Proven as pure_forall.1
bi.pure_implIris.BI.pure_imp
bi.pure_impl_1Proven as pure_imp.1
bi.pure_impl_2Proven as pure_imp.2
bi.wand_curryIris.BI.wand_curry
▶derived_laws_later.v[src]15/125 (12%)
Rocq NameStatusDetails
bi.Timeless_proper
bi.bi_except_0_and_homomorphism
bi.bi_except_0_or_homomorphism
bi.bi_except_0_sep_entails_homomorphism
bi.bi_except_0_sep_entails_weak_homomorphism
bi.bi_except_0_sep_homomorphism
bi.bi_except_0_sep_weak_homomorphism
bi.bi_laterN_and_homomorphism
bi.bi_laterN_or_homomorphism
bi.bi_laterN_sep_entails_homomorphism
bi.bi_laterN_sep_entails_weak_homomorphism
bi.bi_laterN_sep_homomorphism
bi.bi_laterN_sep_weak_homomorphism
bi.bi_later_monoid_and_homomorphism
bi.bi_later_monoid_or_homomorphism
bi.bi_later_monoid_sep_entails_homomorphism
bi.bi_later_monoid_sep_entails_weak_homomorphism
bi.bi_later_monoid_sep_homomorphism
bi.bi_later_monoid_sep_weak_homomorphism
bi.except_0_True
bi.except_0_absorbing
bi.except_0_absorbingly
bi.except_0_affinely_2
bi.except_0_and
bi.except_0_emp
bi.except_0_exist
bi.except_0_exist_2
bi.except_0_flip_mono'
bi.except_0_forall
bi.except_0_frame_l
bi.except_0_frame_r
bi.except_0_idemp
bi.except_0_into_later
bi.except_0_intro
bi.except_0_intuitionistically_2
bi.except_0_intuitionistically_if_2
bi.except_0_later
bi.except_0_laterN
bi.except_0_mono
bi.except_0_mono'
bi.except_0_ne
bi.except_0_or
bi.except_0_persistent
bi.except_0_persistently
bi.except_0_proper
bi.except_0_sep
bi.laterN_0
bi.laterN_True
bi.laterN_absorbing
bi.laterN_absorbingly
bi.laterN_add
bi.laterN_affinely_2
bi.laterN_and
bi.laterN_emp
bi.laterN_exist
bi.laterN_exist_2
bi.laterN_flip_mono'
bi.laterN_forall
bi.laterN_iff
bi.laterN_impl
bi.laterN_intro
bi.laterN_intuitionistically_2
bi.laterN_intuitionistically_if_2
bi.laterN_iter
bi.laterN_later
bi.laterN_le
bi.laterN_mono
bi.laterN_mono'
bi.laterN_ne
bi.laterN_or
bi.laterN_persistent
bi.laterN_persistently
bi.laterN_proper
bi.laterN_sep
bi.laterN_wand
bi.later_True
bi.later_absorbing
bi.later_absorbingly
bi.later_affinely
bi.later_affinely_1
bi.later_affinely_2
bi.later_and
bi.later_contractive_bi_löb
bi.later_emp
bi.later_exist
bi.later_exist_2
bi.later_exist_except_0
bi.later_flip_mono'
bi.later_forall
bi.later_iff
bi.later_impl
bi.later_intuitionistically
bi.later_intuitionistically_2
bi.later_intuitionistically_if
bi.later_intuitionistically_if_2
bi.later_laterN
bi.later_mono'
bi.later_or
bi.later_persistent
bi.later_persistently
bi.later_proper
bi.later_sep
bi.later_wand
bi.later_wand_iff
bi.löb
bi.löb_alt_strong
bi.löb_alt_wand
bi.löb_wand
bi.löb_wand_intuitionistically
bi.not_not_later_False
bi.absorbingly_timelessIris.BI.absorbingly_timeless
bi.affinely_timelessIris.BI.affinely_timeless
bi.and_timelessIris.BI.and_timeless
bi.emp_timelessIris.BI.emp_timeless
bi.exist_timelessIris.BI.exists_timeless
bi.forall_timelessIris.BI.forall_timeless
bi.from_option_timelessIris.BI.from_option_timeless
bi.impl_timelessIris.BI.impl_timeless
bi.intuitionistically_timelessIris.BI.intuitionistically_timeless
bi.or_timelessIris.BI.or_timeless
bi.persistently_timelessIris.BI.persistently_timeless
bi.pure_timelessIris.BI.pure_timeless
bi.sep_timelessIris.BI.sep_timeless
bi.timeless_altIris.BI.timeless_alt
bi.wand_timelessIris.BI.wand_timeless
▶embedding.v[src]0/77 (0%)
Rocq NameStatusDetails
BiEmbed
BiEmbedBUpd
BiEmbedEmp
BiEmbedFUpd
BiEmbedLater
BiEmbedMixin
BiEmbedSbi
Embed
embed_absorbing
embed_absorbingly
embed_absorbingly_if
embed_affine
embed_affinely
embed_affinely_2
embed_affinely_if
embed_affinely_if_2
embed_and
embed_and_homomorphism
embed_bi_embed
embed_big_sepL
embed_big_sepL_2
embed_big_sepM
embed_big_sepMS
embed_big_sepMS_2
embed_big_sepM_2
embed_big_sepS
embed_big_sepS_2
embed_embed
embed_embed_alt
embed_embed_bupd
embed_embed_emp
embed_embed_fupd
embed_embed_later
embed_embed_sbi
embed_embedding_mixin
embed_emp
embed_emp_2
embed_emp_valid
embed_emp_valid_inj
embed_entails_inj
embed_except_0
embed_exist
embed_exist_1
embed_flip_mono
embed_forall
embed_forall_2
embed_iff
embed_impl
embed_impl_2
embed_inj
embed_internal_eq
embed_internal_inj
embed_intuitionistically
embed_intuitionistically_2
embed_intuitionistically_if
embed_intuitionistically_if_2
embed_laterN
embed_mono
embed_ne
embed_or
embed_or_homomorphism
embed_persistent
embed_persistently
embed_persistently_if
embed_plain
embed_plainly
embed_plainly_if
embed_proper
embed_pure
embed_sep
embed_sep_entails_homomorphism
embed_sep_homomorphism
embed_si_pure
embed_timeless
embed_wand
embed_wand_2
embed_wand_iff
▶extensions.v[src]6/6 (100%)
Rocq NameStatusDetails
BiAffineIris.BI.BIAffine
BiLaterContractiveIris.BI.BILaterContractive
BiLöbIris.BI.BILoeb
BiPersistentlyForallIris.BI.BIPersistentlyForall
BiPositiveIris.BI.BIPositive
BiPureForallBIPureForall is provable for all BIs using classical logic, see pure_forall_2
▶interface.v[src]0/60 (0%)
Rocq NameStatusDetails
BiLaterMixin
BiMixin
BiPersistentlyMixin
Import.bi
Import.bi.and_elim_l
Import.bi.and_elim_r
Import.bi.and_intro
Import.bi.and_ne
Import.bi.emp_sep_1
Import.bi.emp_sep_2
Import.bi.entails_po
Import.bi.equiv_entails
Import.bi.exist_elim
Import.bi.exist_intro
Import.bi.exist_ne
Import.bi.forall_elim
Import.bi.forall_intro
Import.bi.forall_ne
Import.bi.impl_elim_l'
Import.bi.impl_intro_r
Import.bi.impl_ne
Import.bi.later_exist_false
Import.bi.later_false_em
Import.bi.later_forall_2
Import.bi.later_intro
Import.bi.later_mono
Import.bi.later_ne
Import.bi.later_persistently_1
Import.bi.later_persistently_2
Import.bi.later_sep_1
Import.bi.later_sep_2
Import.bi.or_elim
Import.bi.or_intro_l
Import.bi.or_intro_r
Import.bi.or_ne
Import.bi.persistently_absorbing
Import.bi.persistently_and_2
Import.bi.persistently_and_sep_elim
Import.bi.persistently_emp_2
Import.bi.persistently_exist_1
Import.bi.persistently_idemp_2
Import.bi.persistently_mono
Import.bi.persistently_ne
Import.bi.pure_elim'
Import.bi.pure_intro
Import.bi.pure_ne
Import.bi.sep_assoc'
Import.bi.sep_comm'
Import.bi.sep_mono
Import.bi.sep_ne
Import.bi.wand_elim_l'
Import.bi.wand_intro_r
Import.bi.wand_ne
Import.bi_cofe
Import.bi_emp_valid
Import.bi_inhabited
Import.bi_ofeO
Import.bi_rewrite_relation
bi_later_mixin_id
bi_persistently_mixin_discrete
▶internal_eq.v[src]45/49 (92%)
Rocq NameStatusDetails
internal_eq_proper
sbi_prop_ext_mixin
sigT_equivI
sum_equivI
absorbingly_internal_eqIris.BI.absorbingly_internalEq
affinely_internal_eq_wand_iffIris.BI.affinely_internalEq_wandIff
contractive_internal_eqIris.BI.contractive_internalEq
csum_equivIIris.BI.csum_equivI
discrete_eqIris.BI.discrete_eq
discrete_eq_1Iris.BI.discrete_eq_mp
discrete_fun_equivIIris.BI.discreteFun_equivI
eq_timelessIris.BI.eq_timeless
equiv_internal_eqIris.BI.internalEq.of_equiv
excl_equivIIris.BI.excl_equivI_excl
f_equivIIris.BI.internalEq.of_internalEquiv_ne
f_equivI_contractiveIris.BI.f_equivI_contractive
fun_extIIris.BI.fun_extI
internal_eqIris.internalEq
internal_eq_absorbingIris.BI.internalEq_absorbing
internal_eq_entailsIris.BI.internalEq_entails
internal_eq_iffIris.BI.internalEq_iff
internal_eq_neIris.BI.internalEq.instInternalEq_ne
internal_eq_persistentIris.BI.internalEq_persistent
internal_eq_reflIris.BI.internalEq.refl
internal_eq_rewriteIris.BI.internalEq.rewrite
internal_eq_rewrite'Iris.BI.internalEq.rewrite'
internal_eq_rewrite_contractiveIris.BI.internalEq_rewrite_contractive
internal_eq_rewrite_contractive'Iris.BI.internalEq_rewrite_contractive'
internal_eq_soundnessIris.BI.internalEq_soundness
internal_eq_symIris.BI.internalEq.symm
internal_eq_transIris.BI.internalEq.trans
internal_eq_wand_iffIris.BI.internalEq_wandIff
later_equivIIris.BI.later_equivI
later_equivI_1Iris.BI.later_equivI_mp
later_equivI_2Iris.BI.later_equivI_mpr
later_equivI_prop_2Iris.BI.later_equivI_prop_mpr
ne_2_internal_eqIris.BI.ne_2_internalEq
ne_internal_eqIris.BI.ne_internalEq
ofe_morO_equivIIris.BI.ofeMorO_equivI
option_equivIIris.BI.option_some_equivI
persistently_internal_eqIris.BI.persistently_internalEq
prod_equivIIris.BI.prod_equivI
prop_ext_si_emp_validIris.BI.prop_ext_siEmpValid_equiv
prop_ext_si_emp_valid_2Iris.BI.prop_ext_siEmpValid_mpr
pure_internal_eqIris.BI.internalEq.of_pure
sbi_later_contractiveIris.BI.sbi_later_contractive
si_pure_internal_eqIris.BI.siPure_internalEq
sig_equivIIris.BI.sig_equivI
sig_equivI_1Iris.BI.sig_equivI_mp
▶lib/atomic.v[src]0/25 (0%)
Rocq NameStatusDetails
aacc_aacc
aacc_aupd
aacc_aupd_abort
aacc_aupd_commit
aacc_intro
atomic_acc
atomic_acc_mask
atomic_acc_mask_weaken
atomic_acc_ne
atomic_acc_wand
atomic_update
atomic_update_aux
atomic_update_def
atomic_update_mask_weaken
atomic_update_ne
atomic_update_pre
atomic_update_pre_mono
atomic_update_unseal
aupd_aacc
aupd_intro
aupd_unfold
elim_acc_aacc
elim_mod_aupd
elim_modal_acc
tac_aupd_intro
▶lib/core.v[src]0/12 (0%)
Rocq NameStatusDetails
coreP
coreP_affine
coreP_elim
coreP_entails
coreP_entails'
coreP_flip_mono
coreP_intro
coreP_mono
coreP_ne
coreP_persistent
coreP_proper
coreP_wand
▶lib/counterexamples.v[src]0/41 (0%)
Rocq NameStatusDetails
affine_em.and_sep
affine_em.sep_dup
inv.A
inv.A_alloc
inv.A_persistent
inv.B
inv.I
inv.P
inv.contradiction
inv.contradiction'
inv.elim_fupd0_fupd1
inv.elim_fupd_fupd
inv.exists_split_fupd0
inv.finished_contradiction
inv.fupd_frame_r
inv.fupd_mono'
inv.fupd_proper
inv.inv_fupd'
inv.invariant_contradiction
inv.mask
inv.saved
inv.saved_A
inv.saved_NA
inv.saved_alloc
inv.saved_cast
inv.saved_persistent
linear.elim_fupd_fupd
linear.fupd_frame_r
linear.fupd_mono'
linear.fupd_proper
linear.leak
linear.mask
löb_em.later_anything
löb_em.later_inconsistent
savedprop.A
savedprop.A_alloc
savedprop.bupd_mono'
savedprop.contradiction
savedprop.elim_modal_bupd
savedprop.saved_A
savedprop.saved_NA
▶lib/fixpoint_banach.v[src]0/8 (0%)
Rocq NameStatusDetails
fixpoint_absorbing
fixpoint_affine
fixpoint_persistent
fixpoint_persistent_absoring
fixpoint_persistent_affine
fixpoint_plain
fixpoint_plain_absoring
fixpoint_plain_affine
▶lib/fixpoint_mono.v[src]0/31 (0%)
Rocq NameStatusDetails
BiMonoPred
Private_paco_mono
Private_wf_pred_mono
bi_greatest_fixpoint
bi_least_fixpoint
greatest_fixpoint_absorbing
greatest_fixpoint_coind
greatest_fixpoint_coiter
greatest_fixpoint_ne
greatest_fixpoint_ne'
greatest_fixpoint_ne_outer
greatest_fixpoint_paco
greatest_fixpoint_proper
greatest_fixpoint_strong_mono
greatest_fixpoint_unfold
greatest_fixpoint_unfold_1
greatest_fixpoint_unfold_2
least_fixpoint_absorbing
least_fixpoint_affine
least_fixpoint_ind
least_fixpoint_ind_wf
least_fixpoint_iter
least_fixpoint_ne
least_fixpoint_ne'
least_fixpoint_persistent_absorbing
least_fixpoint_persistent_affine
least_fixpoint_proper
least_fixpoint_strong_mono
least_fixpoint_unfold
least_fixpoint_unfold_1
least_fixpoint_unfold_2
▶lib/fractional.v[src]0/34 (0%)
Rocq NameStatusDetails
AsFractional
Fractional
Fractional_proper
FrameFractionalQp
as_fractional_embed
combine_sep_as_fractional
combine_sep_as_fractional_half
fractional_as_fractional
fractional_big_sepL
fractional_big_sepL2
fractional_big_sepM
fractional_big_sepMS
fractional_big_sepS
fractional_embed
fractional_half
fractional_internal_fractional
fractional_merge
fractional_sep
fractional_split
frame_fractional
frame_fractional_qp_add_l
frame_fractional_qp_add_r
frame_fractional_qp_half
from_sep_fractional
from_sep_fractional_half
internal_fractional
internal_fractional_affine
internal_fractional_iff
internal_fractional_ne
internal_fractional_persistent
internal_fractional_proper
into_sep_fractional
into_sep_fractional_half
persistent_fractional
▶lib/laterable.v[src]0/32 (0%)
Rocq NameStatusDetails
IntoLaterable
Laterable
big_sepL_laterable
big_sep_sepL_laterable
exist_laterable
from_modal_make_laterable
into_laterable_fallback
into_laterable_laterable
intuitionistic_laterable
later_laterable
laterable_alt
laterable_proper
make_laterable
make_laterable_elim
make_laterable_except_0
make_laterable_flip_mono'
make_laterable_idemp
make_laterable_intro
make_laterable_intro'
make_laterable_intuitionistic_wand
make_laterable_laterable
make_laterable_mono
make_laterable_mono'
make_laterable_ne
make_laterable_proper
make_laterable_sep
make_laterable_wand
modality_make_laterable
modality_make_laterable_mixin
persistent_laterable
sep_laterable
timeless_laterable
▶lib/relations.v[src]0/51 (0%)
Rocq NameStatusDetails
bi_nsteps
bi_nsteps_O
bi_nsteps_add_inv
bi_nsteps_inv_r
bi_nsteps_l
bi_nsteps_ne
bi_nsteps_once
bi_nsteps_once_inv
bi_nsteps_proper
bi_nsteps_r
bi_nsteps_timeless
bi_nsteps_trans
bi_rtc
bi_rtc_affine
bi_rtc_ind_l
bi_rtc_inv
bi_rtc_l
bi_rtc_ne
bi_rtc_nsteps
bi_rtc_once
bi_rtc_persistent
bi_rtc_pre
bi_rtc_pre_mono
bi_rtc_proper
bi_rtc_r
bi_rtc_refl
bi_rtc_strong_ind_l
bi_rtc_tc
bi_rtc_timeless
bi_rtc_trans
bi_rtc_unfold
bi_tc
bi_tc_absorbing
bi_tc_affine
bi_tc_ind_l
bi_tc_l
bi_tc_ne
bi_tc_nsteps
bi_tc_once
bi_tc_persistent
bi_tc_pre
bi_tc_pre_mono
bi_tc_proper
bi_tc_r
bi_tc_rtc
bi_tc_rtc_l
bi_tc_rtc_r
bi_tc_strong_ind_l
bi_tc_timeless
bi_tc_trans
bi_tc_unfold
▶monpred.v[src]0/276 (0%)
Rocq NameStatusDetails
BiIndexBottom
Export.Import.Objective
Export.Import.absorbingly_if_objective
Export.Import.absorbingly_objective
Export.Import.affinely_if_objective
Export.Import.affinely_objective
Export.Import.and_objective
Export.Import.big_sepL_objective
Export.Import.big_sepMS_objective
Export.Import.big_sepM_objective
Export.Import.big_sepS_objective
Export.Import.bupd_objective
Export.Import.embed_objective
Export.Import.emp_objective
Export.Import.except0_objective
Export.Import.exists_objective
Export.Import.forall_objective
Export.Import.fupd_objective
Export.Import.impl_objective
Export.Import.internal_eq_objective
Export.Import.intuitionistically_if_objective
Export.Import.intuitionistically_objective
Export.Import.laterN_objective
Export.Import.later_objective
Export.Import.monPred_absorbing
Export.Import.monPred_affine
Export.Import.monPred_at_absorbing
Export.Import.monPred_at_absorbingly
Export.Import.monPred_at_absorbingly_if
Export.Import.monPred_at_affine
Export.Import.monPred_at_affinely
Export.Import.monPred_at_affinely_if
Export.Import.monPred_at_and
Export.Import.monPred_at_big_sepL
Export.Import.monPred_at_big_sepM
Export.Import.monPred_at_big_sepMS
Export.Import.monPred_at_big_sepS
Export.Import.monPred_at_bupd
Export.Import.monPred_at_embed
Export.Import.monPred_at_emp
Export.Import.monPred_at_except_0
Export.Import.monPred_at_exist
Export.Import.monPred_at_flip_mono
Export.Import.monPred_at_forall
Export.Import.monPred_at_fupd
Export.Import.monPred_at_impl
Export.Import.monPred_at_in
Export.Import.monPred_at_internal_eq
Export.Import.monPred_at_intuitionistically
Export.Import.monPred_at_intuitionistically_if
Export.Import.monPred_at_later
Export.Import.monPred_at_laterN
Export.Import.monPred_at_mono
Export.Import.monPred_at_monoid_and_homomorphism
Export.Import.monPred_at_monoid_or_homomorphism
Export.Import.monPred_at_monoid_sep_homomorphism
Export.Import.monPred_at_objectively
Export.Import.monPred_at_or
Export.Import.monPred_at_persistent
Export.Import.monPred_at_persistently
Export.Import.monPred_at_persistently_if
Export.Import.monPred_at_plain
Export.Import.monPred_at_plainly
Export.Import.monPred_at_pure
Export.Import.monPred_at_sep
Export.Import.monPred_at_subjectively
Export.Import.monPred_at_timeless
Export.Import.monPred_at_wand
Export.Import.monPred_emp_unfold
Export.Import.monPred_equivI
Export.Import.monPred_impl_force
Export.Import.monPred_in_absorbing
Export.Import.monPred_in_elim
Export.Import.monPred_in_flip_mono
Export.Import.monPred_in_intro
Export.Import.monPred_in_mono
Export.Import.monPred_in_persistent
Export.Import.monPred_in_proper
Export.Import.monPred_in_timeless
Export.Import.monPred_internal_eq_unfold
Export.Import.monPred_objectively_absorbing
Export.Import.monPred_objectively_affine
Export.Import.monPred_objectively_and
Export.Import.monPred_objectively_big_sepL
Export.Import.monPred_objectively_big_sepL_entails
Export.Import.monPred_objectively_big_sepM
Export.Import.monPred_objectively_big_sepMS
Export.Import.monPred_objectively_big_sepMS_entails
Export.Import.monPred_objectively_big_sepM_entails
Export.Import.monPred_objectively_big_sepS
Export.Import.monPred_objectively_big_sepS_entails
Export.Import.monPred_objectively_elim
Export.Import.monPred_objectively_embed
Export.Import.monPred_objectively_emp
Export.Import.monPred_objectively_exist
Export.Import.monPred_objectively_flip_mono'
Export.Import.monPred_objectively_forall
Export.Import.monPred_objectively_idemp
Export.Import.monPred_objectively_mono
Export.Import.monPred_objectively_mono'
Export.Import.monPred_objectively_monoid_and_homomorphism
Export.Import.monPred_objectively_monoid_sep_entails_homomorphism
Export.Import.monPred_objectively_monoid_sep_homomorphism
Export.Import.monPred_objectively_ne
Export.Import.monPred_objectively_or
Export.Import.monPred_objectively_persistent
Export.Import.monPred_objectively_plain
Export.Import.monPred_objectively_proper
Export.Import.monPred_objectively_pure
Export.Import.monPred_objectively_sep
Export.Import.monPred_objectively_sep_2
Export.Import.monPred_objectively_timeless
Export.Import.monPred_objectively_unfold
Export.Import.monPred_persistent
Export.Import.monPred_pure_unfold
Export.Import.monPred_si_emp_valid_unfold
Export.Import.monPred_si_pure_unfold
Export.Import.monPred_subjectively_absorbing
Export.Import.monPred_subjectively_affine
Export.Import.monPred_subjectively_and
Export.Import.monPred_subjectively_exist
Export.Import.monPred_subjectively_flip_mono'
Export.Import.monPred_subjectively_forall
Export.Import.monPred_subjectively_idemp
Export.Import.monPred_subjectively_intro
Export.Import.monPred_subjectively_mono
Export.Import.monPred_subjectively_mono'
Export.Import.monPred_subjectively_ne
Export.Import.monPred_subjectively_or
Export.Import.monPred_subjectively_persistent
Export.Import.monPred_subjectively_plain
Export.Import.monPred_subjectively_proper
Export.Import.monPred_subjectively_sep
Export.Import.monPred_subjectively_timeless
Export.Import.monPred_subjectively_unfold
Export.Import.monPred_wand_force
Export.Import.objective_objectively
Export.Import.objective_subjectively
Export.Import.objectively_objective
Export.Import.or_objective
Export.Import.persistently_if_objective
Export.Import.persistently_objective
Export.Import.plainly_if_objective
Export.Import.plainly_objective
Export.Import.pure_objective
Export.Import.sep_objective
Export.Import.si_pure_objective
Export.Import.subjectively_objective
Export.Import.wand_objective
Export.monPredI
Export.monPred_and
Export.monPred_and_aux
Export.monPred_and_def
Export.monPred_and_unseal
Export.monPred_bi_affine
Export.monPred_bi_bupd
Export.monPred_bi_bupd_fupd
Export.monPred_bi_bupd_sbi
Export.monPred_bi_embed
Export.monPred_bi_embed_bupd
Export.monPred_bi_embed_emp
Export.monPred_bi_embed_fupd
Export.monPred_bi_embed_later
Export.monPred_bi_embed_sbi
Export.monPred_bi_fupd
Export.monPred_bi_fupd_sbi
Export.monPred_bi_later_contractive
Export.monPred_bi_later_mixin
Export.monPred_bi_löb
Export.monPred_bi_mixin
Export.monPred_bi_persistently_forall
Export.monPred_bi_persistently_mixin
Export.monPred_bi_positive
Export.monPred_bi_pure_forall
Export.monPred_bupd
Export.monPred_bupd_aux
Export.monPred_bupd_def
Export.monPred_bupd_mixin
Export.monPred_bupd_unseal
Export.monPred_embed
Export.monPred_embed_aux
Export.monPred_embed_def
Export.monPred_embed_unseal
Export.monPred_embedding_mixin
Export.monPred_emp
Export.monPred_emp_aux
Export.monPred_emp_def
Export.monPred_emp_unseal
Export.monPred_entails
Export.monPred_exist
Export.monPred_exist_aux
Export.monPred_exist_def
Export.monPred_exist_unseal
Export.monPred_forall
Export.monPred_forall_aux
Export.monPred_forall_def
Export.monPred_forall_unseal
Export.monPred_fupd
Export.monPred_fupd_aux
Export.monPred_fupd_def
Export.monPred_fupd_mixin
Export.monPred_fupd_unseal
Export.monPred_impl
Export.monPred_impl_aux
Export.monPred_impl_def
Export.monPred_impl_unseal
Export.monPred_in
Export.monPred_in_aux
Export.monPred_in_def
Export.monPred_in_unseal
Export.monPred_later
Export.monPred_later_aux
Export.monPred_later_def
Export.monPred_later_unseal
Export.monPred_objectively
Export.monPred_objectively_aux
Export.monPred_objectively_def
Export.monPred_objectively_unseal
Export.monPred_or
Export.monPred_or_aux
Export.monPred_or_def
Export.monPred_or_unseal
Export.monPred_persistently
Export.monPred_persistently_aux
Export.monPred_persistently_def
Export.monPred_persistently_unseal
Export.monPred_pure
Export.monPred_pure_aux
Export.monPred_pure_def
Export.monPred_pure_unseal
Export.monPred_sbi
Export.monPred_sbi_emp_valid_exist
Export.monPred_sbi_mixin
Export.monPred_sbi_prop_ext_mixin
Export.monPred_sep
Export.monPred_sep_aux
Export.monPred_sep_def
Export.monPred_sep_unseal
Export.monPred_si_emp_valid
Export.monPred_si_emp_valid_aux
Export.monPred_si_emp_valid_def
Export.monPred_si_emp_valid_unseal
Export.monPred_si_pure
Export.monPred_si_pure_aux
Export.monPred_si_pure_def
Export.monPred_si_pure_unseal
Export.monPred_subjectively
Export.monPred_subjectively_aux
Export.monPred_subjectively_def
Export.monPred_subjectively_unseal
Export.monPred_unseal
Export.monPred_unseal_bi
Export.monPred_upclosed
Export.monPred_wand
Export.monPred_wand_aux
Export.monPred_wand_def
Export.monPred_wand_unseal
biIndex
monPred
monPredO
monPred_at_ne
monPred_at_proper
monPred_cofe
monPred_dist
monPred_dist'
monPred_equiv
monPred_equiv'
monPred_ofe_mixin
monPred_sig
monPred_sig_monPred
monPred_sig_ne
monPred_sig_proper
sig_monPred
sig_monPred_ne
sig_monPred_proper
sig_monPred_sig
▶plainly.v[src]89/155 (57%)
Rocq NameStatusDetails
Plain_proper
absorbingly_elim_plainly
affinely_plainly_elim
and_sep_plainly
big_sepM2_empty_plain
big_sepM2_plain
big_sepM2_plainly
big_sepMS_empty_plain
big_sepMS_plain
big_sepMS_plainly
impl_wand_affinely_plainly
impl_wand_plainly
impl_wand_plainly_2
internal_eq_plain
internal_eq_timeless
intuitionistically_plainly
intuitionistically_plainly_elim
later_plainly_1
later_plainly_2
persistently_wand_affinely_plainly
plainly
plainly_True_alt
plainly_absorbing
plainly_affinely_elim
plainly_and
plainly_and_emp_elim
plainly_and_sep
plainly_and_sep_assoc
plainly_and_sep_elim
plainly_and_sep_l
plainly_and_sep_l_1
plainly_and_sep_r
plainly_and_sep_r_1
plainly_elim
plainly_emp
plainly_emp_2
plainly_entails_l
plainly_entails_r
plainly_exist
plainly_flip_mono'
plainly_forall
plainly_idemp
plainly_idemp_1
plainly_if_flip_mono'
plainly_if_mono'
plainly_if_proper
plainly_if_sep_2
plainly_impl
plainly_impl_wand
plainly_impl_wand_2
plainly_into_absorbingly
plainly_intro'
plainly_mono'
plainly_or
plainly_or_2
plainly_proper
plainly_pure
plainly_sep
plainly_sep_2
plainly_sep_dup
plainly_sep_entails_homomorphism
plainly_sep_entails_weak_homomorphism
plainly_timeless
plainly_wand
plainly_wand_affinely_plainly
prop_ext_2
PlainIris.BI.Plain
absorbingly_plainIris.BI.absorbingly_plain
affinely_plainIris.BI.affinely_plain
and_plainIris.BI.and_plain
big_andL_nil_plainIris.BI.big_andL_nil_plain
big_andL_plainIris.BI.big_andL_plain
big_andL_plainlyIris.BI.bigAndL_plainly
big_orL_nil_plainIris.BI.big_orL_nil_plain
big_orL_plainIris.BI.big_orL_plain
big_orL_plainlyIris.BI.bigOrL_plainly
big_sepL2_nil_plainIris.BI.bigSepL2_nil_plain
big_sepL2_plainIris.BI.bigSepL2_plain
big_sepL2_plainlyIris.BI.bigSepL2_plainly
big_sepL_nil_plainIris.BI.big_sepL_nil_plain
big_sepL_plainIris.BI.big_sepL_plain
big_sepL_plainlyIris.BI.bigSepL_plainly
big_sepM_empty_plainIris.BI.bigSepM_empty_plain
big_sepM_plainIris.BI.bigSepM__plain
big_sepM_plainlyIris.BI.bigSepM_plainly
big_sepS_empty_plainIris.BI.bigSepS_empty_plain
big_sepS_plainIris.BI.bigSepS_plain
big_sepS_plainlyIris.BI.bigSepS_plainly
emp_plainIris.BI.emp_plain
except_0_plainIris.BI.except0_plain
except_0_plainlyIris.BI.except0_plainly
except_0_plainly_1Iris.BI.except0_plainly_1
exist_plainIris.BI.exists_plain
forall_plainIris.BI.forall_plain
from_option_plainIris.BI.from_option_plain
impl_persistentIris.BI.impl_persistent
impl_plainIris.BI.impl_plain
intuitionistically_plainIris.BI.intuitionistically_plain
laterN_plainIris.BI.laterN_plain
laterN_plainlyIris.BI.laterN_plainly
laterN_plainly_ifIris.BI.laterN_plainlyIf
later_plainIris.BI.later_plain
later_plainlyIris.later_plainly
later_plainly_ifIris.BI.later_plainlyIf
limit_preserving_PlainIris.BI.limitPreserving_plain
or_plainIris.BI.or_plain
persistently_elim_plainlyIris.BI.persistently_elim_plainly
persistently_if_elim_plainlyIris.BI.persistently_if_elim_plainly
persistently_impl_plainlyIris.persistently_impl_plainly
persistently_plainIris.BI.persistently_plain
plain_persistentIris.BI.plain_persistent
plain_plainlyIris.BI.plain_plainly
plain_plainly_2Iris.BI.plain_plainly_2
plainly_True_empIris.BI.plainly_true_emp
plainly_absorbIris.plainly_absorb
plainly_altIris.BI.plainly_alt
plainly_alt_absorbingIris.BI.plainly_alt_absorbing
plainly_and_homomorphismIris.BI.plainly_and_homomorphism
plainly_elim_persistentlyIris.plainly_elim_persistently
plainly_emp_introIris.plainly_emp_intro
plainly_exist_1Iris.plainly_exist_1
plainly_exist_2Iris.BI.plainly_exists_2
plainly_forall_2Iris.plainly_forall_2
plainly_idemp_2Iris.plainly_idemp_2
plainly_ifIris.BI.BIBase.Plainly.plainlyIf
plainly_if_absorbingIris.BI.plainly_if_absorbing
plainly_if_andIris.BI.plainly_if_and
plainly_if_existIris.BI.plainly_if_exists
plainly_if_exist_2Iris.BI.plainly_if_exists_2
plainly_if_idempIris.BI.plainly_if_idemp
plainly_if_monoIris.plainly_if_mono
plainly_if_neIris.instPlainlyIf_ne
plainly_if_orIris.BI.plainly_if_or
plainly_if_or_2Iris.BI.plainly_if_or_2
plainly_if_pureIris.BI.plainly_if_pure
plainly_impl_plainlyIris.plainly_impl_plainly
plainly_internal_eqIris.BI.plainly_internalEq
plainly_introIris.BI.plainly_intro
plainly_monoIris.plainly_mono
plainly_neIris.instPlainly_ne
plainly_or_homomorphismIris.BI.plainly_or_homomorphism
plainly_persistentIris.BI.plainly_persistent
plainly_persistently_elimIris.BI.plainly_persistently_elim
plainly_plainIris.BI.plainly_plain
plainly_sep_homomorphismIris.BI.plainly_sep_homomorphism
plainly_sep_weak_homomorphismIris.BI.plainly_sep_weak_homomorphism
plainly_si_pureIris.BI.plainly_siPure
prop_extIris.BI.prop_ext
pure_plainIris.BI.pure_plain
sep_plainIris.BI.sep_plain
siProp_plainIris.instPlainlySbi
si_emp_valid_plainIris.BI.si_emp_valid_plain
si_pure_plainIris.BI.si_pure_plain
wand_persistentIris.BI.wand_persistent
wand_plainIris.BI.wand_plain
▶sbi.v[src]59/72 (82%)
Rocq NameStatusDetails
SbiMixin
SbiPropExtMixin
SiEmpValid
SiPure
si_emp_valid_affinely_2
si_emp_valid_flip_mono'
si_emp_valid_mono'
si_emp_valid_proper
si_pure_absorbing
si_pure_flip_mono'
si_pure_mono'
siprop_sbi_mixin
siprop_sbi_prop_ext_mixin
SbiIris.Sbi
SbiEmpValidExistIris.SbiEmpValidExist
absorbingly_si_pureIris.absorbingly_siPure
affinely_si_pure_si_emp_validIris.affinely_siPure_siEmpValid
laterN_soundnessIris.laterN_soundness
later_soundnessIris.later_soundness
persistently_impl_si_pureUPred.persistently_imp_uPredSiPure
persistently_si_pureIris.persistently_siPure
pure_soundnessIris.pure_soundness
si_emp_valid_affinelyIris.siEmpValid_affinely
si_emp_valid_andIris.siEmpValid_and
si_emp_valid_empIris.siEmpValid_emp
si_emp_valid_emp_validIris.siEmpValid_emp_valid
si_emp_valid_except_0Iris.siEmpValid_except0
si_emp_valid_existIris.siEmpValid_exist
si_emp_valid_exist_2Iris.siEmpValid_exist_mpr
si_emp_valid_forallIris.siEmpValid_forall
si_emp_valid_impl_si_pureIris.siEmpValid_imp_siPure
si_emp_valid_intuitionisticallyIris.siEmpValid_intuitionistically
si_emp_valid_laterIris.siEmpValid_later
si_emp_valid_laterNIris.siEmpValid_laterN
si_emp_valid_later_1UPred.uPredSiEmpValid_later_mp
si_emp_valid_monoUPred.uPredSiEmpValid_mono
si_emp_valid_neUPred.uPredSiEmpValid_ne
si_emp_valid_orIris.siEmpValid_or
si_emp_valid_or_2Iris.siEmpValid_or_mpr
si_emp_valid_persistentlyIris.siEmpValid_persistently
si_emp_valid_pureIris.siEmpValid_pure
si_emp_valid_sepIris.siEmpValid_sep
si_emp_valid_si_pureUPred.uPredSiEmpValid_uPredSiPure
si_emp_valid_timelessIris.siEmpValid_timeless
si_emp_valid_wand_si_pureIris.siEmpValid_wand_siPure
si_pure_andIris.siPure_and
si_pure_and_sepIris.siPure_and_sep
si_pure_emp_validIris.siPure_emp_valid
si_pure_entailsIris.siPure_entails
si_pure_except_0Iris.siPure_except0
si_pure_existIris.siPure_exist
si_pure_forallIris.siPure_forall
si_pure_forall_2Iris.siPure_forall_mpr
si_pure_iffIris.siPure_iff
si_pure_implIris.siPure_imp
si_pure_impl_2UPred.uPredSiPure_imp_mpr
si_pure_impl_iff_wandIris.siPure_iff_wandIff
si_pure_impl_wandIris.siPure_imp_wand
si_pure_injIris.siPure_inj
si_pure_laterUPred.uPredSiPure_later
si_pure_laterNIris.siPure_laterN
si_pure_monoUPred.uPredSiPure_mono
si_pure_neUPred.uPredSiPure_ne
si_pure_orIris.siPure_or
si_pure_persistentIris.siPure_persistent
si_pure_properIris.siPure_mono_bi
si_pure_pureIris.siPure_pure
si_pure_si_emp_validUPred.uPredSiPure_uPredSiEmpValid
si_pure_si_emp_valid_elimIris.siPure_siEmpValid_elim
si_pure_timelessIris.siPure_timeless
siprop_sbiIris.instSbiSiProp
siprop_sbi_emp_valid_existIris.instSbiEmpValidExistSiProp
▶sbi_unfold.v[src]0/26 (0%)
Rocq NameStatusDetails
SbiUnfold
SbiUnfold_closed
SbiUnfold_downclose
sbi_unfold_and
sbi_unfold_closed_weaken
sbi_unfold_closure_indicator.sbi_unfold_closure_indicator
sbi_unfold_emp_valid
sbi_unfold_entails
sbi_unfold_equiv
sbi_unfold_exist
sbi_unfold_forall
sbi_unfold_iff
sbi_unfold_iff_wand
sbi_unfold_impl
sbi_unfold_internal_cmra_valid
sbi_unfold_internal_eq
sbi_unfold_internal_included
sbi_unfold_later
sbi_unfold_maybe_downclose
sbi_unfold_or
sbi_unfold_pure
sbi_unfold_sep
sbi_unfold_si_pure
sbi_unfold_siprop
sbi_unfold_tceq
sbi_unfold_wand
▶telescopes.v[src]0/15 (0%)
Rocq NameStatusDetails
bi_texist
bi_texist_absorbing
bi_texist_affine
bi_texist_exist
bi_texist_ne
bi_texist_persistent
bi_texist_proper
bi_texist_timeless
bi_tforall
bi_tforall_absorbing
bi_tforall_forall
bi_tforall_ne
bi_tforall_persistent
bi_tforall_proper
bi_tforall_timeless
▶updates.v[src]6/113 (5%)
Rocq NameStatusDetails
BUpd
BiBUpd
BiBUpdFUpd
BiBUpdMixin
BiBUpdSbi
BiFUpd
BiFUpdMixin
BiFUpdSbi
FUpd
big_sepL2_fupd
big_sepL_bupd
big_sepL_fupd
big_sepM2_bupd
big_sepM2_fupd
big_sepMS_bupd
big_sepMS_fupd
big_sepM_bupd
big_sepM_fupd
big_sepS_bupd
big_sepS_fupd
bupd_absorbing
bupd_and
bupd_elim
bupd_exist
bupd_flip_mono'
bupd_forall
bupd_frame_l
bupd_frame_r
bupd_idemp
bupd_intro
bupd_mono
bupd_mono'
bupd_ne
bupd_or
bupd_or_homomorphism
bupd_plain
bupd_plain_forall
bupd_plainly
bupd_plainly_elim
bupd_proper
bupd_sep
bupd_sep_homomorphism
bupd_trans
bupd_wand_l
bupd_wand_r
except_0_bupd
except_0_fupd
fupd_absorbing
fupd_and
fupd_elim
fupd_except_0
fupd_exist
fupd_flip_mono'
fupd_forall
fupd_frame_l
fupd_frame_r
fupd_idemp
fupd_intro
fupd_mask_frame
fupd_mask_frame_acc
fupd_mask_frame_r
fupd_mask_frame_r'
fupd_mask_intro
fupd_mask_intro_discard
fupd_mask_intro_subseteq
fupd_mask_mono
fupd_mask_subseteq
fupd_mask_subseteq_emptyset_difference
fupd_mask_weaken
fupd_mono
fupd_mono'
fupd_ne
fupd_or
fupd_or_homomorphism
fupd_plain_forall
fupd_plain_forall'
fupd_plain_forall_2
fupd_plain_keep
fupd_plain_keep_l
fupd_plain_keep_r
fupd_plain_laterN
fupd_plainly_elim
fupd_plainly_forall_2
fupd_plainly_keep_l
fupd_plainly_keep_r
fupd_plainly_later
fupd_plainly_laterN
fupd_proper
fupd_sep
fupd_sep_homomorphism
fupd_trans
fupd_trans_frame
fupd_wand_l
fupd_wand_r
step_fupdN_S_fupd
step_fupdN_add
step_fupdN_frame_l
step_fupdN_intro
step_fupdN_le
step_fupdN_mono
step_fupdN_wand
step_fupd_frame_l
step_fupd_intro
step_fupd_mask_frame_r
step_fupd_mask_mono
step_fupd_plain_forall
step_fupd_wand
fupd_plain_laterIris.fupd_plain_later
fupd_plain_maskIris.fupd_plain_mask
fupd_plainly_maskIris.fupd_plainly_mask
step_fupdN_plainIris.step_fupdN_plain
step_fupd_fupdIris.step_fupd_fupd
step_fupd_plainIris.step_fupd_plain
▶weakestpre.v[src]0/5 (0%)
Rocq NameStatusDetails
Twp
Wp
stuckness
stuckness_le
stuckness_le_po
▶program_logic/0/299 (0%)
▶adequacy.v[src]0/17 (0%)
Rocq NameStatusDetails
adequate
adequate_alt
adequate_tp_safe
steps_sum
wp_adequacy
wp_adequacy_gen
wp_invariance
wp_invariance_gen
wp_not_stuck
wp_progress_gen
wp_step
wp_strong_adequacy
wp_strong_adequacy_gen
wptp_postconditions
wptp_preservation
wptp_progress
wptp_step
▶atomic.v[src]0/7 (0%)
Rocq NameStatusDetails
atomic_seq_wp_atomic
atomic_wp
atomic_wp_inv
atomic_wp_mask_weaken
atomic_wp_seq
atomic_wp_seq_step
persistent_seq_wp_atomic
▶ectx_language.v[src]0/42 (0%)
Rocq NameStatusDetails
EctxLanguageMixin
Ectx_step'
LanguageOfEctx
base_atomic
base_irreducible
base_prim_fill_reducible
base_prim_fill_reducible_no_obs
base_prim_irreducible
base_prim_reducible
base_prim_reducible_no_obs
base_prim_step
base_redex_unique
base_reducible
base_reducible_no_obs
base_reducible_no_obs_reducible
base_reducible_prim_step
base_reducible_prim_step_ctx
base_step_not_stuck
base_stuck
base_stuck_stuck
ectxLanguage
ectx_lang
ectx_lang_ctx
ectx_lang_mixin
ectx_language_atomic
fill_comp
fill_empty
fill_inj
fill_prim_step
fill_reducible
fill_reducible_no_obs
fill_val
not_base_reducible
prim_base_irreducible
prim_base_reducible
prim_step
pure_base_step
pure_base_step_pure_step
pure_exec_fill
step_by_val
sub_redexes_are_values
val_base_stuck
▶ectx_lifting.v[src]0/10 (0%)
Rocq NameStatusDetails
wp_lift_atomic_base_step
wp_lift_atomic_base_step_fupd
wp_lift_atomic_base_step_no_fork
wp_lift_atomic_base_step_no_fork_fupd
wp_lift_base_step
wp_lift_base_step_fupd
wp_lift_base_stuck
wp_lift_pure_base_stuck
wp_lift_pure_det_base_step_no_fork
wp_lift_pure_det_base_step_no_fork'
▶ectxi_language.v[src]0/15 (0%)
Rocq NameStatusDetails
EctxLanguageOfEctxi
EctxiLanguageMixin
base_ctx_step_val
ectxiLanguage
ectxi_lang
ectxi_lang_ctx_item
ectxi_lang_ectx
ectxi_lang_ectx_mixin
ectxi_language_sub_redexes_are_values
fill
fill_app
fill_item_inj
fill_item_no_val_inj
fill_item_val
fill_not_val
▶language.v[src]0/55 (0%)
Rocq NameStatusDetails
AsVal
Atomic
IntoVal
LanguageCtx
LanguageMixin
PureExec
as_val_is_Some
as_vals_of_val
atomicity
cfg
erased_step
erased_step_Permutation
erased_step_pure_step_tp
erased_steps_nsteps
exprO
irreducible
irreducible_fill
irreducible_fill_inv
language
language_ctx_id
not_not_stuck
not_reducible
not_stuck
not_stuck_fill_inv
nsteps
of_to_val
of_to_val_flip
of_val_inj
prim_step_not_stuck
pure_exec_ctx
pure_step
pure_step_ctx
pure_step_nsteps_ctx
reducible
reducible_fill
reducible_fill_inv
reducible_no_obs
reducible_no_obs_fill
reducible_no_obs_fill_inv
reducible_no_obs_reducible
reducible_not_val
rtc_pure_step_ctx
rtc_pure_step_val
stateO
step
step_Permutation
step_insert
strongly_atomic_atomic
stuck
stuck_fill
stuckness_to_atomicity
to_of_val
valO
val_irreducible
val_stuck
▶lifting.v[src]0/11 (0%)
Rocq NameStatusDetails
wp_lift_atomic_step
wp_lift_atomic_step_fupd
wp_lift_pure_det_step_no_fork
wp_lift_pure_step_no_fork
wp_lift_pure_stuck
wp_lift_step
wp_lift_step_fupd
wp_lift_step_fupdN
wp_lift_stuck
wp_pure_step_fupd
wp_pure_step_later
▶ownp.v[src]0/26 (0%)
Rocq NameStatusDetails
ownP
ownPGS
ownPG_irisGS
ownPGpreS
ownP_adequacy
ownP_eq
ownP_invariance
ownP_lift_atomic_base_step
ownP_lift_atomic_det_base_step
ownP_lift_atomic_det_base_step_no_fork
ownP_lift_atomic_det_step
ownP_lift_atomic_det_step_no_fork
ownP_lift_atomic_step
ownP_lift_base_step
ownP_lift_base_stuck
ownP_lift_pure_base_step
ownP_lift_pure_det_base_step_no_fork
ownP_lift_pure_det_step_no_fork
ownP_lift_pure_step
ownP_lift_step
ownP_lift_stuck
ownP_state_twice
ownP_timeless
ownPΣ
reducible_not_val_inhabitant
subG_ownPΣ
▶total_adequacy.v[src]0/11 (0%)
Rocq NameStatusDetails
twp_total
twp_twptp
twptp
twptp_Permutation
twptp_app
twptp_ind
twptp_pre
twptp_pre_mono
twptp_pre_mono'
twptp_total
twptp_unfold
▶total_ectx_lifting.v[src]0/5 (0%)
Rocq NameStatusDetails
twp_lift_atomic_base_step
twp_lift_atomic_base_step_no_fork
twp_lift_base_step
twp_lift_pure_base_step_no_fork
twp_lift_pure_det_base_step_no_fork
▶total_lifting.v[src]0/5 (0%)
Rocq NameStatusDetails
twp_lift_atomic_step
twp_lift_pure_det_step_no_fork
twp_lift_pure_step_no_fork
twp_lift_step
twp_pure_step
▶total_weakestpre.v[src]0/44 (0%)
Rocq NameStatusDetails
add_modal_fupd_twp
elim_acc_twp_atomic
elim_modal_bupd_twp
elim_modal_fupd_twp
elim_modal_fupd_twp_atomic
elim_modal_fupd_twp_atomic_wrong_mask
elim_modal_fupd_twp_wrong_mask
frame_twp
fupd_twp
twp'
twp_atomic
twp_aux
twp_bind
twp_bind_inv
twp_def
twp_frame_l
twp_frame_r
twp_frame_wand
twp_fupd
twp_ind
twp_mask_mono
twp_mono
twp_mono'
twp_ne
twp_pre
twp_pre'
twp_pre_mono
twp_pre_mono'
twp_proper
twp_strong_mono
twp_stuck_mono
twp_stuck_weaken
twp_unfold
twp_unseal
twp_value
twp_value'
twp_value_fupd
twp_value_fupd'
twp_wand
twp_wand_l
twp_wand_r
twp_wp
twp_wp_fupdN_strong
twp_wp_step
▶weakestpre.v[src]0/51 (0%)
Rocq NameStatusDetails
add_modal_fupd_wp
elim_acc_wp_atomic
elim_acc_wp_nonatomic
elim_modal_bupd_wp
elim_modal_fupd_wp
elim_modal_fupd_wp_atomic
elim_modal_fupd_wp_atomic_wrong_mask
elim_modal_fupd_wp_wrong_mask
frame_wp
fupd_wp
irisGS_gen
is_except_0_wp
wp'
wp_atomic
wp_aux
wp_bind
wp_bind_inv
wp_contractive
wp_credit_access
wp_def
wp_flip_mono'
wp_frame_l
wp_frame_r
wp_frame_step_l
wp_frame_step_l'
wp_frame_step_r
wp_frame_step_r'
wp_frame_wand
wp_fupd
wp_mask_mono
wp_mono
wp_mono'
wp_ne
wp_pre
wp_pre_contractive
wp_proper
wp_step_fupd
wp_step_fupdN
wp_step_fupdN_strong
wp_strong_mono
wp_stuck_mono
wp_stuck_weaken
wp_unfold
wp_unseal
wp_value
wp_value'
wp_value_fupd
wp_value_fupd'
wp_wand
wp_wand_l
wp_wand_r
▶proofmode/264/1046 (25%)
▶base.v[src]0/25 (0%)
Rocq NameStatusDetails
Export.beq_eq_dec
Export.ident
Export.ident_beq
Export.ident_beq_reflect
Export.ident_beq_true
Export.maybe_IAnon
Export.maybe_INamed
Export.pm_app
Export.pm_from_option
Export.pm_option_bind
Export.pm_option_fun
Export.positive_beq
Export.positive_beq_true
Pos_succ
ascii_beq
ascii_beq_true
beq
beq_true
direction
lazy_andb_true
negb
negb_true
string_beq
string_beq_reflect
string_beq_true
▶class_instances.v[src]137/208 (66%)
Rocq NameStatusDetails
add_modal_forall
add_modal_tforall
add_modal_wand
add_modal_wandM
as_emp_valid_tforall
combine_sep_as_absorbingly
combine_sep_as_affinely
combine_sep_as_intuitionistically
combine_sep_as_persistently
elim_inv_acc_with_close
elim_inv_acc_without_close
elim_modal_tforall
elim_modal_wandM
from_and_big_sepL2_app_persistent
from_and_big_sepL2_cons_persistent
from_and_big_sepL_app_persistent
from_and_big_sepL_cons_persistent
from_and_big_sepMS_disj_union_persistent
from_and_pure_iff
from_assumption_tforall
from_exist_exist
from_exist_texist
from_forall_tforall
from_pure_big_sepL
from_pure_big_sepM
from_pure_big_sepMS
from_pure_big_sepS
from_pure_texist
from_pure_tforall
from_sep_big_sepL2_app
from_sep_big_sepL2_cons
from_sep_big_sepL_app
from_sep_big_sepL_cons
from_sep_big_sepMS_disj_union
from_sep_pure_iff
from_tforall_pure
from_wand_wandM
into_exist_texist
into_forall_impl
into_forall_impl_pure
into_forall_tforall
into_forall_wand
into_pure_big_sepL
into_pure_big_sepM
into_pure_big_sepMS
into_pure_big_sepS
into_pure_forall
into_pure_pure_wand
into_pure_texist
into_pure_tforall
into_sep_affinely
into_sep_big_sepL2_cons
into_sep_big_sepL_app
into_sep_big_sepL_cons
into_sep_big_sepMS_disj_union
into_sep_intuitionistically
into_sep_persistently
into_wand_affine_args
into_wand_forall_prop_false
into_wand_forall_prop_true
into_wand_impl_false_false
into_wand_impl_false_true
into_wand_impl_true_false
into_wand_impl_true_true
into_wand_tforall
into_wand_wand
into_wand_wandM
maybe_combine_sep_as_absorbingly
maybe_combine_sep_as_affinely
maybe_combine_sep_as_intuitionistically
maybe_combine_sep_as_persistently
AndIntoSepIris.ProofMode.AndIntoSep
as_emp_valid_emp_validIris.ProofMode.asEmpValidEmpValid
as_emp_valid_entailsIris.ProofMode.asEmpValid_entails
as_emp_valid_equivIris.ProofMode.asEmpValid_equiv
as_emp_valid_forallIris.ProofMode.asEmpValid_forall
elim_modal_absorbingly_hereIris.ProofMode.elimModal_absorbingly_here
elim_modal_forallIris.ProofMode.elimModal_forall
elim_modal_wandIris.ProofMode.elimModal_wand
from_affinely_affineIris.ProofMode.fromAffinely_affine
from_affinely_defaultIris.ProofMode.fromAffinely_default
from_affinely_intuitionisticallyIris.ProofMode.fromAffinely_intuitionistically
from_and_andIris.ProofMode.fromAnd_and
from_and_persistentlyIris.ProofMode.fromAnd_persistently
from_and_persistently_sepIris.ProofMode.fromAnd_persistently_sep
from_and_pureIris.ProofMode.fromAnd_pure
from_and_sep_persistent_lIris.ProofMode.fromAnd_sep_persistent_l
from_and_sep_persistent_rIris.ProofMode.fromAnd_sep_persistent_r
from_assumption_absorbingly_rIris.ProofMode.fromAssumption_absorbingly_r
from_assumption_affinely_l_trueIris.ProofMode.fromAssumption_affinely_l
from_assumption_affinely_rIris.ProofMode.fromAssumption_affinely_r
from_assumption_exactIris.ProofMode.fromAssumption_exact
from_assumption_forallIris.ProofMode.fromAssumption_forall
from_assumption_intuitionistically_lIris.ProofMode.fromAssumption_intuitionistically_l
from_assumption_intuitionistically_l_trueIris.ProofMode.fromAssumption_intuitionistically_l_true
from_assumption_intuitionistically_rIris.ProofMode.fromAssumption_intuitionistically_r
from_assumption_persistently_l_falseIris.ProofMode.fromAssumption_persistently_l_false
from_assumption_persistently_l_trueIris.ProofMode.fromAssumption_persistently_l_true
from_assumption_persistently_rIris.ProofMode.fromAssumption_persistently_r
from_exist_absorbinglyIris.ProofMode.fromExists_absorbingly
from_exist_affinelyIris.ProofMode.fromExists_affinely
from_exist_intuitionisticallyIris.ProofMode.fromExists_intuitionistically
from_exist_persistentlyIris.ProofMode.fromExists_persistently
from_exist_pureIris.ProofMode.fromExists_pure
from_forall_forallIris.ProofMode.fromForall_forall
from_forall_impl_pureIris.ProofMode.fromForall_imp_pure
from_forall_intuitionisticallyIris.ProofMode.fromForall_intuitionistically
from_forall_persistentlyIris.ProofMode.fromForall_persistently
from_forall_pureIris.ProofMode.fromForall_pure
from_forall_pure_notIris.ProofMode.fromForall_pure_not
from_forall_wand_pureIris.ProofMode.fromForall_wand_pure
from_impl_implIris.ProofMode.fromImp_imp
from_modal_absorbinglyIris.ProofMode.fromModal_absorbingly
from_modal_affinelyIris.ProofMode.fromModal_affinely
from_modal_intuitionisticallyIris.ProofMode.fromModal_intuitionistically
from_modal_intuitionistically_affine_biIris.ProofMode.fromModal_intuitionistically_affine_bi
from_modal_persistentlyIris.ProofMode.fromModal_persistently
from_or_absorbinglyIris.ProofMode.fromOr_absorbingly
from_or_affinelyIris.ProofMode.fromOr_affinely
from_or_intuitionisticallyIris.ProofMode.fromOr_intuitionistically
from_or_orIris.ProofMode.fromOr_or
from_or_persistentlyIris.ProofMode.fromOr_persistently
from_or_pureIris.ProofMode.fromOr_pure
from_pure_absorbinglyIris.ProofMode.fromPure_absorbingly
from_pure_affinely_trueIris.ProofMode.fromPure_affinely_true
from_pure_empIris.ProofMode.fromPure_emp
from_pure_existIris.ProofMode.fromPure_exists
from_pure_forallIris.ProofMode.fromPure_forall
from_pure_intuitionistically_trueIris.ProofMode.fromPure_intuitionistically_true
from_pure_persistentlyIris.ProofMode.fromPure_persistently
from_pure_pureIris.ProofMode.fromPure_pure
from_pure_pure_andIris.ProofMode.fromPure_pure_and
from_pure_pure_implIris.ProofMode.fromPure_pure_imp
from_pure_pure_orIris.ProofMode.fromPure_pure_or
from_pure_pure_sep_trueIris.ProofMode.fromPure_pure_sep_true
from_pure_pure_wandIris.ProofMode.fromPure_pure_wand_true
from_sep_absorbinglyIris.ProofMode.fromSep_absorbingly
from_sep_affinelyIris.ProofMode.fromSep_affinely
from_sep_andIris.ProofMode.fromSep_and
from_sep_intuitionisticallyIris.ProofMode.fromSep_intuitionistically
from_sep_persistentlyIris.ProofMode.fromSep_persistently
from_sep_pureIris.ProofMode.fromSep_pure
from_sep_sepIris.ProofMode.fromSep_sep
from_wand_wandIris.ProofMode.fromWand_wand
into_absorbingly_TrueIris.ProofMode.intoAbsorbingly_true
into_absorbingly_absorbingIris.ProofMode.intoAbsorbingly_absorbing
into_absorbingly_defaultIris.ProofMode.intoAbsorbingly_default
into_absorbingly_intuitionisticallyIris.ProofMode.intoAbsorbingly_intuitionistically
into_and_affinelyIris.ProofMode.intoAnd_affinely
into_and_andIris.ProofMode.intoAnd_and
into_and_and_affine_lIris.ProofMode.intoAnd_and_affine_l
into_and_and_affine_rIris.ProofMode.intoAnd_and_affine_r
into_and_intuitionisticallyIris.ProofMode.intoAnd_intuitionistically
into_and_persistentlyIris.ProofMode.intoAnd_persistently
into_and_pureIris.ProofMode.intoAnd_pure
into_and_sepIris.ProofMode.intoAnd_sep
into_and_sep_affineIris.ProofMode.intoAnd_sep_affine
into_exist_absorbinglyIris.ProofMode.intoExists_absorbingly
into_exist_affinelyIris.ProofMode.intoExists_affinely
into_exist_and_pureIris.ProofMode.intoExist_and_pure
into_exist_existIris.ProofMode.intoExists_exists
into_exist_intuitionisticallyIris.ProofMode.intoExists_intuitionistically
into_exist_persistentlyIris.ProofMode.intoExists_persistently
into_exist_pureIris.ProofMode.intoExists_pure
into_exist_sep_pureIris.ProofMode.intoExist_sep_pure
into_forall_affinelyIris.ProofMode.intoForall_affinely
into_forall_forallIris.ProofMode.intoForall_forall
into_forall_intuitionisticallyIris.ProofMode.intoForall_intuitionistically
into_forall_persistentlyIris.ProofMode.intoForall_persistently
into_forall_wand_pureIris.ProofMode.intoForall_wand_pure
into_or_absorbinglyIris.ProofMode.intoOr_absorbingly
into_or_affinelyIris.ProofMode.intoOr_affinely
into_or_intuitionisticallyIris.ProofMode.intoOr_intuitionistically
into_or_orIris.ProofMode.intoOr_or
into_or_persistentlyIris.ProofMode.intoOr_persistently
into_or_pureIris.ProofMode.intoOr_pure
into_persistent_affinelyIris.ProofMode.intoPersistently_affinely
into_persistent_hereIris.ProofMode.intoPersistently_self
into_persistent_intuitionisticallyIris.ProofMode.intoPersistently_intuitionistically
into_persistent_persistentIris.ProofMode.intoPersistently_persistent
into_persistent_persistentlyIris.ProofMode.intoPersistently_persistently
into_pure_absorbinglyIris.ProofMode.intoPure_absorbingly
into_pure_affinelyIris.ProofMode.intoPure_affinely
into_pure_existIris.ProofMode.intoPure_exists
into_pure_intuitionisticallyIris.ProofMode.intoPure_intuitionistically
into_pure_persistentlyIris.ProofMode.intoPure_persistently
into_pure_pureIris.ProofMode.intoPure_pure
into_pure_pure_andIris.ProofMode.intoPure_pure_and
into_pure_pure_implIris.ProofMode.intoPure_pure_imp
into_pure_pure_orIris.ProofMode.intoPure_pure_or
into_pure_pure_sepIris.ProofMode.intoPure_pure_sep
into_sep_affinely_trimIris.ProofMode.intoSep_affinely_trim
into_sep_and_persistent_lIris.ProofMode.intoSep_and_persistent_l
into_sep_and_persistent_rIris.ProofMode.intoSep_and_persistent_r
into_sep_intuitionistically_affineIris.ProofMode.intoSep_intuitionistically_affine
into_sep_persistently_affineIris.ProofMode.intoSep_persistently_affine
into_sep_pureIris.ProofMode.intoSep_pure
into_sep_sepIris.ProofMode.intoSep_sep
into_wand_affineIris.ProofMode.intoWand_affinely
into_wand_and_lIris.ProofMode.intoWand_and_l
into_wand_and_rIris.ProofMode.intoWand_and_r
into_wand_forallIris.ProofMode.intoWand_forall
into_wand_impl'IntoWand' is not used in Lean
into_wand_intuitionisticallyIris.ProofMode.intoWand_intuitionistically
into_wand_persistently_falseIris.ProofMode.intoWand_persistently_false
into_wand_persistently_trueIris.ProofMode.intoWand_persistently_true
into_wand_wand'IntoWand' is not used in Lean
into_wand_wandM'IntoWand' is not used in Lean
▶class_instances_cmra.v[src]0/6 (0%)
Rocq NameStatusDetails
from_exist_internal_included
from_pure_internal_cmra_valid
from_pure_internal_included
into_exist_internal_included
into_pure_internal_cmra_valid
into_pure_internal_included
▶class_instances_embedding.v[src]0/41 (0%)
Rocq NameStatusDetails
add_modal_embed_bupd_goal
add_modal_embed_fupd_goal
as_emp_valid_embed
combine_sep_gives_embed
elim_modal_embed_bupd_goal
elim_modal_embed_bupd_hyp
elim_modal_embed_fupd_goal
elim_modal_embed_fupd_hyp
from_and_embed
from_exist_embed
from_forall_embed
from_impl_embed
from_modal_affinely_embed
from_modal_embed
from_modal_id_embed
from_modal_intuitionistically_embed
from_modal_later_embed
from_modal_persistently_embed
from_modal_plainly_embed
from_or_embed
from_pure_embed
from_sep_embed
from_wand_embed
into_and_embed
into_embed_affinely
into_embed_embed
into_except_0_embed
into_exist_embed
into_forall_embed
into_internal_eq_embed
into_inv_embed
into_later_embed
into_or_embed
into_persistent_embed
into_pure_embed
into_sep_embed
into_wand_affine_embed_false
into_wand_affine_embed_true
into_wand_embed
is_except_0_embed
maybe_combine_sep_as_embed
▶class_instances_frame.v[src]0/40 (0%)
Rocq NameStatusDetails
GatherEvarsEq
TCCbnTele
frame_absorbingly
frame_affinely
frame_affinely_here
frame_affinely_here_absorbing
frame_and
frame_big_sepL2_app
frame_big_sepL2_cons
frame_big_sepL_app
frame_big_sepL_cons
frame_big_sepMS_disj_union
frame_bupd
frame_embed
frame_eq_embed
frame_except_0
frame_exist
frame_exist_helper
frame_exist_no_instantiate
frame_forall
frame_fupd
frame_here
frame_here_absorbing
frame_here_pure
frame_here_pure_persistent
frame_impl
frame_impl_persistent
frame_intuitionistically
frame_later
frame_laterN
frame_or_persistent
frame_or_spatial
frame_persistently
frame_pure_embed
frame_sep_l
frame_sep_persistent_l
frame_sep_r
frame_texist
frame_tforall
frame_wand
▶class_instances_internal_eq.v[src]0/10 (0%)
Rocq NameStatusDetails
from_modal_Next
from_pure_internal_eq
into_internal_eq_absorbingly
into_internal_eq_affinely
into_internal_eq_internal_eq
into_internal_eq_intuitionistically
into_internal_eq_persistently
into_internal_eq_plainly
into_laterN_Next
into_pure_eq
▶class_instances_later.v[src]68/86 (79%)
Rocq NameStatusDetails
add_modal_except_0
add_modal_except_0_later
add_modal_later
add_modal_later_except_0
into_laterN_big_sepL
into_laterN_big_sepL2
into_laterN_big_sepM
into_laterN_big_sepM2
into_laterN_big_sepMS
into_laterN_big_sepS
into_laterN_laterN_bool
into_sep_affinely_later
maybe_combine_sep_as_except_0
maybe_combine_sep_as_later
maybe_combine_sep_as_laterN
maybe_combine_sep_gives_except_0
maybe_combine_sep_gives_later
maybe_combine_sep_gives_laterN
elim_modal_timelessIris.ProofMode.elimModal_timeless
from_and_except_0Iris.ProofMode.fromAnd_except0
from_and_laterIris.ProofMode.fromAnd_later
from_and_laterNIris.ProofMode.fromAnd_laterN
from_assumption_except_0Iris.ProofMode.fromAssumption_except0
from_assumption_laterIris.ProofMode.fromAssumption_later
from_assumption_laterNIris.ProofMode.fromAssumption_laterN
from_exist_except_0Iris.ProofMode.fromExists_except0
from_exist_laterIris.ProofMode.fromExists_later
from_exist_laterNIris.ProofMode.fromExists_laterN
from_forall_except_0Iris.ProofMode.fromForall_except0
from_forall_laterIris.ProofMode.fromForall_later
from_forall_laterNIris.ProofMode.fromForall_laterN
from_modal_except_0Iris.ProofMode.fromModal_except0
from_modal_laterIris.ProofMode.fromModal_later
from_modal_laterNIris.ProofMode.fromModal_laterN
from_or_except_0Iris.ProofMode.fromOr_except0
from_or_laterIris.ProofMode.fromOr_later
from_or_laterNIris.ProofMode.fromOr_laterN
from_pure_except_0Iris.ProofMode.fromPure_except0
from_pure_laterIris.ProofMode.fromPure_later
from_pure_laterNIris.ProofMode.fromPure_laterN
from_sep_except_0Iris.ProofMode.fromSep_except0
from_sep_laterIris.ProofMode.fromSep_later
from_sep_laterNIris.ProofMode.fromSep_laterN
into_and_except_0Iris.ProofMode.intoAnd_except0
into_and_laterIris.ProofMode.intoAnd_later
into_and_laterNIris.ProofMode.intoAnd_laterN
into_except_0_absorbinglyIris.ProofMode.intoExcept0_absorbingly
into_except_0_affinelyIris.ProofMode.intoExcept0_affinely
into_except_0_except_0Iris.ProofMode.intoExcept0_except0
into_except_0_intuitionisticallyIris.ProofMode.intoExcept0_intuitionistically
into_except_0_laterIris.ProofMode.intoExcept0_later
into_except_0_later_ifIris.ProofMode.intoExcept0_laterIf
into_except_0_persistentlyIris.ProofMode.intoExcept0_persistently
into_exist_except_0Iris.ProofMode.intoExists_except0
into_exist_laterIris.ProofMode.intoExists_later
into_exist_laterNIris.ProofMode.intoExists_laterN
into_forall_except_0Iris.ProofMode.intoForall_except0
into_forall_laterIris.ProofMode.intoForall_later
into_forall_laterNIris.ProofMode.intoForall_laterN
into_laterN_0Iris.ProofMode.intoLaterN_default_0
into_laterN_and_lIris.ProofMode.intoLaterN_and
into_laterN_and_rIris.ProofMode.intoLaterN_and
into_laterN_existIris.ProofMode.intoLaterN_exists
into_laterN_forallIris.ProofMode.intoLaterN_forall
into_laterN_laterIris.ProofMode.intoLaterN_later
into_laterN_laterNIris.ProofMode.intoLaterN_laterN
into_laterN_or_lIris.ProofMode.intoLaterN_or
into_laterN_or_rIris.ProofMode.intoLaterN_or
into_laterN_sep_lIris.ProofMode.intoLaterN_sep
into_laterN_sep_rIris.ProofMode.intoLaterN_sep
into_later_absorbinglyIris.ProofMode.intoLaterN_absorbingly
into_later_affinelyIris.ProofMode.intoLaterN_affinely
into_later_intuitionisticallyIris.ProofMode.intoLaterN_intuitionistically
into_later_persistentlyIris.ProofMode.intoLaterN_persistently
into_or_except_0Iris.ProofMode.intoOr_except0
into_or_laterIris.ProofMode.intoOr_later
into_or_laterNIris.ProofMode.intoOr_laterN
into_sep_except_0Iris.ProofMode.intoSep_except0
into_sep_laterIris.ProofMode.intoSep_later
into_sep_laterNIris.ProofMode.intoSep_laterN
into_wand_laterIris.ProofMode.intoWand_later
into_wand_laterNIris.ProofMode.intoWand_laterN
into_wand_laterN_argsIntoWand' is not used in Lean
into_wand_later_argsIntoWand' is not used in Lean
is_except_0_except_0Iris.ProofMode.isExcept0_except0
is_except_0_laterIris.ProofMode.isExcept0_later
▶class_instances_make.v[src]0/49 (0%)
Rocq NameStatusDetails
False_quick_affine
absorbingly_quick_absorbing
affinely_quick_affine
bi_affine_quick_absorbing
bi_affine_quick_affine
emp_quick_affine
intuitionistically_quick_affine
make_absorbingly_absorbing
make_absorbingly_default
make_absorbingly_emp
make_affinely_True
make_affinely_affine
make_affinely_default
make_and_default
make_and_emp_l
make_and_emp_r
make_and_false_l
make_and_false_r
make_and_true_l
make_and_true_r
make_embed_default
make_embed_emp
make_embed_pure
make_except_0_True
make_except_0_default
make_intuitionistically_True
make_intuitionistically_True_affine
make_intuitionistically_default
make_intuitionistically_emp
make_laterN_default
make_laterN_emp
make_laterN_true
make_or_default
make_or_emp_l
make_or_emp_r
make_or_false_l
make_or_false_r
make_or_true_l
make_or_true_r
make_persistently_True
make_persistently_default
make_persistently_emp
make_sep_default
make_sep_emp_l
make_sep_emp_r
make_sep_true_l
make_sep_true_r
persistently_quick_absorbing
pure_quick_absorbing
▶class_instances_plainly.v[src]20/20 (100%)
Rocq NameStatusDetails
from_and_plainlyIris.ProofMode.fromAnd_plainly
from_assumption_plainly_l_falseIris.ProofMode.fromAssumption_plainly_l_false
from_assumption_plainly_l_trueIris.ProofMode.fromAssumption_plainly_l_true
from_exist_plainlyIris.ProofMode.fromExists_plainly
from_forall_plainlyIris.ProofMode.fromForall_plainly
from_modal_plainlyIris.ProofMode.fromModal_plainly
from_or_plainlyIris.ProofMode.fromOr_plainly
from_pure_plainlyIris.ProofMode.fromPure_plainly
from_sep_plainlyIris.ProofMode.fromSep_plainly
into_and_plainlyIris.ProofMode.intoAnd_plainly
into_except_0_plainlyIris.ProofMode.intoExcept0_plainly
into_exist_plainlyIris.ProofMode.intoExists_plainly
into_forall_plainlyIris.ProofMode.intoForall_plainly
into_later_plainlyIris.ProofMode.intoLaterN_plainly
into_or_plainlyIris.ProofMode.intoOr_plainly
into_pure_plainlyIris.ProofMode.intoPure_plainly
into_sep_plainlyIris.ProofMode.intoSep_plainly
into_sep_plainly_affineIris.ProofMode.intoSep_plainly_affine
into_wand_plainly_falseIris.ProofMode.intoWand_plainly_false
into_wand_plainly_trueIris.ProofMode.intoWand_plainly_true
▶class_instances_updates.v[src]31/37 (84%)
Rocq NameStatusDetails
add_modal_bupd
add_modal_fupd
elim_acc_bupd
elim_acc_fupd
from_forall_fupd
from_forall_step_fupd
elim_modal_bupdIris.ProofMode.elimModal_bupd
elim_modal_bupd_fupdIris.ProofMode.elimModal_bupd_fupd
elim_modal_bupd_plainIris.ProofMode.elimModal_bupd_plain
elim_modal_bupd_plain_goalIris.ProofMode.elimModal_bupd_plain_goal
elim_modal_fupd_fupdIris.ProofMode.elimModal_fupd_fupd
elim_modal_fupd_fupd_wrong_maskIris.ProofMode.elimModal_fupd_fupd_wrongMask
from_assumption_bupdIris.ProofMode.fromAssumption_bupd
from_assumption_fupdIris.ProofMode.fromAssumption_fupd
from_exist_bupdIris.ProofMode.fromExists_bupd
from_exist_fupdIris.ProofMode.fromExists_fupd
from_modal_bupdIris.ProofMode.fromModal_bupd
from_modal_fupdIris.ProofMode.fromModal_fupd
from_modal_fupd_wrong_maskIris.ProofMode.fromModal_fupd_wrongMask
from_or_bupdIris.ProofMode.fromOr_bupd
from_or_fupdIris.ProofMode.fromOr_fupd
from_pure_bupdIris.ProofMode.fromPure_bupd
from_pure_fupdIris.ProofMode.fromPure_fupd
from_sep_bupdIris.ProofMode.fromSep_bupd
from_sep_fupdIris.ProofMode.fromSep_fupd
into_and_bupdIris.ProofMode.intoAnd_bupd
into_and_fupdIris.ProofMode.intoAnd_fupd
into_forall_bupdIris.ProofMode.intoForall_bupd
into_forall_fupdIris.ProofMode.intoForall_fupd
into_wand_bupdIris.ProofMode.intoWand_bupd
into_wand_bupd_argsIntoWand' is not used in Lean
into_wand_bupd_persistentIris.ProofMode.intoWand_bupd_persistent
into_wand_fupdIris.ProofMode.intoWand_fupd
into_wand_fupd_argsIntoWand' is not used in Lean
into_wand_fupd_persistentIris.ProofMode.intoWand_fupd_persistent
is_except_0_bupdIris.ProofMode.isExcept0_bupd
is_except_0_fupdIris.ProofMode.isExcept0_fupd
▶classes.v[src]0/85 (0%)
Rocq NameStatusDetails
AddModal
AsEmpValid
AsEmpValid0
CombineSepAs
CombineSepGives
ElimAcc
ElimInv
ElimModal
Frame
FrameInstantiateExistDisabled
FromAffinely
FromAnd
FromAssumption
FromExist
FromForall
FromImpl
FromModal
FromOr
FromPure
FromPureT
FromSep
FromWand
IntoAbsorbingly
IntoAcc
IntoAnd
IntoEmbed
IntoExcept0
IntoExist
IntoForall
IntoInternalEq
IntoInv
IntoLaterN
IntoOr
IntoPersistent
IntoPure
IntoPureT
IntoSep
IntoWand
IntoWand'
IsApp
IsCons
IsDisjUnion
IsExcept0
KnownLFromAssumption
KnownRFromAssumption
MaybeCombineSepAs
MaybeFrame'
MaybeIntoLaterN
accessor
add_modal_id
as_emp_valid_1
as_emp_valid_2
as_emp_valid_direction
elim_inv_tc_opaque
elim_modal_tc_opaque
from_and_tc_opaque
from_exist_tc_opaque
from_forall_tc_opaque
from_modal_tc_opaque
from_or_tc_opaque
from_pureT_hint
from_pure_tc_opaque
from_sep_tc_opaque
from_wand_tc_opaque
into_and_tc_opaque
into_exist_tc_opaque
into_forall_tc_opaque
into_inv_tc_opaque
into_or_tc_opaque
into_pureT_hint
into_pure_tc_opaque
into_sep_tc_opaque
into_wand_tc_opaque
is_app_app
is_cons_cons
is_disj_union_disj_union
maybe_combine_sep_as_combine_sep_as
maybe_combine_sep_as_default
maybe_frame_default
maybe_frame_default_persistent
maybe_frame_frame
maybe_into_laterN_default
maybe_into_laterN_default_0
pm_error
progress_indicator
▶classes_make.v[src]0/25 (0%)
Rocq NameStatusDetails
KnownLMakeAnd
KnownLMakeOr
KnownLMakeSep
KnownMakeAbsorbingly
KnownMakeAffinely
KnownMakeEmbed
KnownMakeExcept0
KnownMakeIntuitionistically
KnownMakeLaterN
KnownMakePersistently
KnownRMakeAnd
KnownRMakeOr
KnownRMakeSep
MakeAbsorbingly
MakeAffinely
MakeAnd
MakeEmbed
MakeExcept0
MakeIntuitionistically
MakeLaterN
MakeOr
MakePersistently
MakeSep
QuickAbsorbing
QuickAffine
▶coq_tactics.v[src]0/99 (0%)
Rocq NameStatusDetails
AffineEnv
CombineSepsAs
CombineSepsAsGives
IntoEmpValid
IntoIH
IntoModalIntuitionisticEnv
IntoModalSpatialEnv
MaybeIntoLaterNEnvs
TransformIntuitionisticEnv
TransformSpatialEnv
affine_env_bi
affine_env_nil
affine_env_snoc
affine_env_spatial
combine_seps_as_from_as_gives
combine_seps_as_gives_nil
combine_seps_as_gives_singleton
combine_seps_gives_cons
combine_seps_gives_of_envs
into_emp_valid_forall
into_emp_valid_here
into_emp_valid_impl
into_emp_valid_proj
into_emp_valid_tforall
into_ih_Forall
into_ih_Forall2
into_ih_entails
into_ih_forall
into_ih_impl
into_laterN_env_sound
into_laterN_envs
tac_accu
tac_and_destruct
tac_and_destruct_choice
tac_and_split
tac_apply
tac_assert
tac_assumption
tac_assumption_coq
tac_clear
tac_combine_as
tac_combine_as_gives
tac_combine_gives
tac_emp_intro
tac_eval
tac_eval_in
tac_ex_falso
tac_exist
tac_exist_destruct
tac_false_destruct
tac_forall_intro
tac_forall_revert
tac_forall_specialize
tac_frame
tac_frame_pure
tac_impl_intro
tac_impl_intro_drop
tac_impl_intro_intuitionistic
tac_intuitionistic
tac_inv_elim
tac_löb
tac_modal_elim
tac_modal_intro
tac_or_destruct
tac_or_l
tac_or_r
tac_pose_proof
tac_pose_proof_hyp
tac_pure
tac_pure_intro
tac_pure_revert
tac_rename
tac_revert
tac_revert_ih
tac_rewrite
tac_rewrite_in
tac_sep_split
tac_spatial
tac_specialize
tac_specialize_assert
tac_specialize_assert_intuitionistic
tac_specialize_assert_pure
tac_specialize_frame
tac_specialize_intuitionistic_helper
tac_specialize_intuitionistic_helper_done
tac_start
tac_stop
tac_unlock
tac_unlock_True
tac_unlock_emp
tac_wand_intro
tac_wand_intro_drop
tac_wand_intro_intuitionistic
transform_intuitionistic_env_nil
transform_intuitionistic_env_snoc
transform_intuitionistic_env_snoc_not
transform_spatial_env_nil
transform_spatial_env_snoc
transform_spatial_env_snoc_not
▶environments.v[src]0/132 (0%)
Rocq NameStatusDetails
Envs_proper
Esnoc_proper
env
env_Forall2
env_Forall2_antisymm
env_Forall2_fresh
env_Forall2_impl
env_Forall2_refl
env_Forall2_sym
env_Forall2_trans
env_Forall2_wf
env_app
env_app_disjoint
env_app_fresh
env_app_fresh_1
env_app_perm
env_app_wf
env_delete
env_delete_fresh
env_delete_wf
env_dom
env_intuitionistic_flip_mono
env_intuitionistic_mono
env_intuitionistic_proper
env_lookup
env_lookup_delete
env_lookup_delete_Some
env_lookup_delete_correct
env_lookup_env_delete
env_lookup_env_delete_ne
env_lookup_perm
env_lookup_snoc
env_lookup_snoc_ne
env_replace
env_replace_fresh
env_replace_lookup
env_replace_perm
env_replace_wf
env_spatial_flip_mono
env_spatial_is_nil
env_spatial_is_nil_intuitionistically
env_spatial_mono
env_spatial_proper
env_subenv
env_subenv_fresh
env_subenv_wf
env_to_list
env_to_list_proper
env_to_list_subenv_proper
env_to_prop
env_to_prop_and
env_to_prop_and_go
env_to_prop_and_pers_sound
env_to_prop_go
env_to_prop_sound
env_wf
envs
envs_Forall2
envs_Forall2_antisymm
envs_Forall2_impl
envs_Forall2_refl
envs_Forall2_sym
envs_Forall2_trans
envs_app
envs_app_singleton_sound
envs_app_sound
envs_clear_intuitionistic
envs_clear_intuitionistic_sound
envs_clear_spatial
envs_clear_spatial_sound
envs_delete
envs_delete_intuitionistic
envs_delete_spatial
envs_dom
envs_entails
envs_entails_flip_mono
envs_entails_mono
envs_entails_proper
envs_entails_unseal
envs_incr_counter
envs_incr_counter_equiv
envs_incr_counter_sound
envs_lookup
envs_lookup_delete
envs_lookup_delete_Some
envs_lookup_delete_list
envs_lookup_delete_list_cons
envs_lookup_delete_list_nil
envs_lookup_delete_list_sound
envs_lookup_delete_sound
envs_lookup_envs_clear_spatial
envs_lookup_envs_delete
envs_lookup_envs_delete_ne
envs_lookup_intuitionistic_sound
envs_lookup_snoc
envs_lookup_snoc_ne
envs_lookup_sound
envs_lookup_sound'
envs_lookup_sound_2
envs_lookup_split
envs_replace
envs_replace_singleton_sound
envs_replace_singleton_sound'
envs_replace_sound
envs_replace_sound'
envs_simple_replace
envs_simple_replace_maybe_sound
envs_simple_replace_singleton_sound
envs_simple_replace_singleton_sound'
envs_simple_replace_sound
envs_simple_replace_sound'
envs_snoc
envs_snoc_sound
envs_split
envs_split_go
envs_split_go_sound
envs_split_sound
envs_wf
envs_wf'
of_envs
of_envs'
of_envs'_alt
of_envs_alt
of_envs_eq
of_envs_mono
of_envs_mono'
of_envs_proper
of_envs_proper'
pre_envs_entails
pre_envs_entails_aux
pre_envs_entails_def
pre_envs_entails_unseal
▶ident_name.v[src]2/2 (100%)
Rocq NameStatusDetails
AsIdentNamefile ignored: Rocq-specific ident name handling
ident_namefile ignored: Rocq-specific ident name handling
▶intro_patterns.v[src]0/10 (0%)
Rocq NameStatusDetails
gallina_ident
intro_pat
intro_pat.big_conj
intro_pat.close
intro_pat.close_conj_list
intro_pat.close_list
intro_pat.parse
intro_pat.parse_go
intro_pat.stack_item
intro_pat_intuitionistic
▶ltac_tactics.v[src]0/3 (0%)
Rocq NameStatusDetails
esel_pat
iTrm
use_tac_specialize_intuitionistic_helper
▶modalities.v[src]0/25 (0%)
Rocq NameStatusDetails
modality
modality_action
modality_and_forall
modality_and_transform
modality_emp
modality_flip_mono'
modality_id
modality_id_mixin
modality_intuitionistic_action_spec
modality_intuitionistic_forall
modality_intuitionistic_forall_big_and
modality_intuitionistic_id
modality_intuitionistic_id_big_and
modality_intuitionistic_transform
modality_mixin
modality_mono
modality_mono'
modality_proper
modality_sep
modality_spatial_action_spec
modality_spatial_clear
modality_spatial_forall
modality_spatial_forall_big_sep
modality_spatial_id
modality_spatial_transform
▶modality_instances.v[src]0/12 (0%)
Rocq NameStatusDetails
modality_affinely
modality_affinely_mixin
modality_embed
modality_embed_mixin
modality_intuitionistically
modality_intuitionistically_mixin
modality_laterN
modality_laterN_mixin
modality_persistently
modality_persistently_mixin
modality_plainly
modality_plainly_mixin
▶monpred.v[src]0/111 (0%)
Rocq NameStatusDetails
FrameMonPredAt
IsBiIndexRel
MakeMonPredAt
add_modal_at_bupd_goal
add_modal_at_fupd_goal
as_emp_valid_monPred_at
as_emp_valid_monPred_at_equiv
as_emp_valid_monPred_at_wand
elim_acc_at_None
elim_acc_at_Some
elim_inv_embed_with_close
elim_inv_embed_without_close
elim_modal_at
elim_modal_at_bupd_goal
elim_modal_at_bupd_hyp
elim_modal_at_fupd_goal
elim_modal_at_fupd_hyp
frame_monPred_at_absorbingly
frame_monPred_at_affinely
frame_monPred_at_and
frame_monPred_at_bupd
frame_monPred_at_embed
frame_monPred_at_enter
frame_monPred_at_exist
frame_monPred_at_forall
frame_monPred_at_fupd
frame_monPred_at_here
frame_monPred_at_impl
frame_monPred_at_intuitionistically
frame_monPred_at_later
frame_monPred_at_laterN
frame_monPred_at_objectively
frame_monPred_at_or
frame_monPred_at_persistently
frame_monPred_at_sep
frame_monPred_at_subjectively
frame_monPred_at_wand
from_and_monPred_at
from_assumption_make_monPred_at_l
from_assumption_make_monPred_at_r
from_assumption_make_monPred_objectively
from_assumption_make_monPred_subjectively
from_exist_monPred_at
from_exist_monPred_at_ex
from_forall_monPred_at
from_forall_monPred_at_impl
from_forall_monPred_at_objectively
from_forall_monPred_at_plainly
from_forall_monPred_at_wand
from_later_monPred_at
from_modal_affinely_monPred_at
from_modal_id_monPred_at
from_modal_intuitionistically_monPred_at
from_modal_objectively
from_modal_persistently_monPred_at
from_modal_subjectively
from_or_monPred_at
from_pure_monPred_at
from_pure_monPred_in
from_sep_monPred_at
into_and_monPred_at
into_embed_objective
into_except_0_monPred_at_bwd
into_except_0_monPred_at_fwd
into_exist_monPred_at
into_exist_monPred_at_ex
into_forall_monPred_at
into_forall_monPred_at_index
into_forall_monPred_at_objectively
into_forall_monPred_at_plainly
into_internal_eq_monPred_at
into_or_monPred_at
into_persistent_monPred_at
into_pure_monPred_at
into_pure_monPred_in
into_sep_monPred_at
into_wand_impl'_monPred
into_wand_monPred_at_known_unknown_ge
into_wand_monPred_at_known_unknown_le
into_wand_monPred_at_unknown_known
into_wand_monPred_at_unknown_unknown
into_wand_wand'_monPred
is_bi_index_rel_refl
is_except_0_monPred_at
make_monPred_at_absorbingly
make_monPred_at_absorbingly_if
make_monPred_at_affinely
make_monPred_at_affinely_if
make_monPred_at_and
make_monPred_at_bupd
make_monPred_at_default
make_monPred_at_embed
make_monPred_at_emp
make_monPred_at_except_0
make_monPred_at_exists
make_monPred_at_forall
make_monPred_at_fupd
make_monPred_at_in
make_monPred_at_internal_eq
make_monPred_at_intuitionistically
make_monPred_at_intuitionistically_if
make_monPred_at_later
make_monPred_at_laterN
make_monPred_at_or
make_monPred_at_persistently
make_monPred_at_persistently_if
make_monPred_at_pure
make_monPred_at_sep
maybe_into_later_monPred_at
modality_objectively
modality_objectively_mixin
▶sel_patterns.v[src]0/4 (0%)
Rocq NameStatusDetails
sel_pat
sel_pat.parse
sel_pat.parse_go
sel_pat_pure
▶spec_patterns.v[src]0/10 (0%)
Rocq NameStatusDetails
goal_kind
goal_kind_modal
spec_goal
spec_pat
spec_pat.close
spec_pat.close_ident
spec_pat.parse
spec_pat.parse_go
spec_pat.stack_item
spec_pat_modal
▶string_ident.v[src]1/1 (100%)
Rocq NameStatusDetails
StringToIdent.coq_string_to_list_bytefile ignored: Rocq-specific string-based ident handling
▶tokens.v[src]5/5 (100%)
Rocq NameStatusDetails
cons_statefile ignored: Rocq-specific tokenizer
statefile ignored: Rocq-specific tokenizer
tokenIris.token
tokenizefile ignored: Rocq-specific tokenizer
tokenize_gofile ignored: Rocq-specific tokenizer
▶si_logic/35/123 (28%)
▶bi.v[src]4/27 (15%)
Rocq NameStatusDetails
siProp.siProp_and_unseal
siProp.siProp_cmra_valid_unseal
siProp.siProp_emp_unseal
siProp.siProp_exist_unseal
siProp.siProp_forall_unseal
siProp.siProp_impl_unseal
siProp.siProp_internal_eq_unseal
siProp.siProp_later_unseal
siProp.siProp_or_unseal
siProp.siProp_persistently_unseal
siProp.siProp_pure_unseal
siProp.siProp_sep_unseal
siProp.siProp_unseal
siProp.siProp_wand_unseal
siProp_bi_later_mixin
siProp_bi_mixin
siProp_bi_persistently_mixin
siProp_emp
siProp_persistently
siProp_plainly
siProp_pure_forall
siProp_sep
siProp_wand
siPropIIris.SiProp.instBI
siProp_affineIris.SiProp.instBIAffine
siProp_later_contractiveIris.SiProp.instBILaterContractive
siProp_persistentIris.SiProp.instPersistent
▶siprop.v[src]31/96 (32%)
Rocq NameStatusDetails
siPropO
siProp_and_aux
siProp_and_def
siProp_and_unseal
siProp_cmra_valid_aux
siProp_cmra_valid_def
siProp_cmra_valid_unseal
siProp_cofe
siProp_compl
siProp_dist
siProp_dist'
siProp_equiv
siProp_equiv'
siProp_exist_aux
siProp_exist_def
siProp_exist_unseal
siProp_forall_aux
siProp_forall_def
siProp_forall_unseal
siProp_impl_aux
siProp_impl_def
siProp_impl_unseal
siProp_internal_eq_aux
siProp_internal_eq_def
siProp_internal_eq_unseal
siProp_later_aux
siProp_later_def
siProp_later_unseal
siProp_ofe_mixin
siProp_or_aux
siProp_or_def
siProp_or_unseal
siProp_primitive.and_elim_l
siProp_primitive.and_elim_r
siProp_primitive.and_intro
siProp_primitive.and_ne
siProp_primitive.entails_anti_symm
siProp_primitive.entails_po
siProp_primitive.equiv_entails
siProp_primitive.exist_elim
siProp_primitive.exist_intro
siProp_primitive.exist_ne
siProp_primitive.forall_elim
siProp_primitive.forall_intro
siProp_primitive.forall_ne
siProp_primitive.impl_elim_l'
siProp_primitive.impl_intro_r
siProp_primitive.impl_ne
siProp_primitive.later_contractive
siProp_primitive.later_exist_false
siProp_primitive.later_false_em
siProp_primitive.later_forall_2
siProp_primitive.later_intro
siProp_primitive.later_mono
siProp_primitive.or_elim
siProp_primitive.or_intro_l
siProp_primitive.or_intro_r
siProp_primitive.or_ne
siProp_primitive.pure_elim'
siProp_primitive.pure_forall_2
siProp_primitive.pure_intro
siProp_primitive.siProp_unseal
siProp_pure_aux
siProp_pure_def
siProp_pure_unseal
SiProp_downcloseIris.SiProp.downClose
siPropIris.SiProp
siProp_andIris.SiProp.and
siProp_cmra_validIris.SiProp.cmraValid
siProp_entailsIris.SiProp.entails
siProp_existIris.SiProp.exist
siProp_forallIris.SiProp.all
siProp_implIris.SiProp.imp
siProp_internal_eqIris.SiProp.internalEq
siProp_laterIris.SiProp.later
siProp_orIris.SiProp.or
siProp_primitive.cmra_valid_elimIris.SiProp.cmraValid_elim
siProp_primitive.cmra_valid_introIris.SiProp.cmraValid_intro
siProp_primitive.cmra_valid_neIris.SiProp.instNonExpansiveCmraValid
siProp_primitive.cmra_valid_weakenIris.SiProp.cmraValid_weaken
siProp_primitive.discrete_eq_1Iris.SiProp.discrete_eq_internalEq
siProp_primitive.fun_extIIris.SiProp.fun_ext_internalEq
siProp_primitive.internal_eq_entailsIris.SiProp.internalEq_entails
siProp_primitive.internal_eq_neIris.SiProp.instNonExpansiveâ‚‚InternalEq
siProp_primitive.internal_eq_reflIris.SiProp.internalEq_refl
siProp_primitive.internal_eq_rewriteIris.SiProp.internalEq_rewrite
siProp_primitive.internal_eq_soundnessIris.SiProp.internalEq_soundness
siProp_primitive.later_equivI_1Iris.SiProp.later_equiv_internalEq_mp
siProp_primitive.later_equivI_2Iris.SiProp.later_equiv_internalEq_mpr
siProp_primitive.later_soundnessIris.SiProp.later_soundness
siProp_primitive.prop_ext_2Iris.SiProp.prop_ext
siProp_primitive.pure_neIris.SiProp.pure_dist_of_iff
siProp_primitive.pure_soundnessIris.SiProp.pure_soundness
siProp_primitive.sig_equivI_1Iris.SiProp.sig_equiv_internalEq
siProp_primitive.valid_entailsIris.SiProp.cmraValid_entails_iff
siProp_pureIris.SiProp.pure
▶Stale Entries3 entries
NameStatusDetails
big_op.big_opL
big_op.big_opM
big_op.big_opS