Iris Porting Status

Use Agree with a typeclass instance instead.

Use the plain Agree type with a typeclass instance instead.

Use Agree.Raw.ext

Defined in Agree OFE instance.

Derivable from instNonExpansive_AgreeMap' with NonExpansive.eqv

Use the CMRA instance instead.

Derivable from Agree.op_ne₂ using NonExpansive₂.eqv

Use the CMRA instance instead.

Use the CMRA instance instead.

Derivable from Agree.validN_ne using NonExpansive.eqv

Use the CMRA instance instead.

Use toAgree_included

Use the general Agree.op_inv theorem

Use the general Agree.op_invN theorem

Use toAgree_op_valid_iff_eq

Use toAgree_op_valid_iff_eq

Derivable from instNonExpansive_toAgree with NonExpansive.eqv

Use the Auth type and View.instOFE typeclass

Use the Auth type and View.instCMRA typeclass

Use the Auth type and View.instUCMRA typeclass

Use auth_dfrac_op_inv

Derivable from auth_ne with NonExpansive.eqv

Inference succeeds automatically

Use frag_op_validN

Use frag_op_validN

Use frag_op_valid

Use frag_op_valid

Derivable from frag_ne with NonExpansive.eqv

Found by typeclass inference from the View.Frag instance

Use frag_validN.mp

Use frag_validN.mpr

Use frag_valid

Use frag_valid

Inference succeeds automatically

Use the IsViewRel typeclass

Use the IsViewRel typeclass

Use the IsViewRel typeclass

Leibniz (=) variant; use bigOpL_hom_weak

Leibniz (=) variant; use bigOpL_hom

Merged into bigOpL_eq

Use bigOpL_dist

Use bigOpL_eq_of_perm

Use bigOpL_eq

Not needed

Leibniz (=) variant; use BigOpMS.hom_weak

Leibniz (=) variant; use BigOpMS.hom

Not needed

Merged into bigOpMS_eq

Use bigOpMS_dist

Use bigOpMS_eq

Not needed

Not needed

Leibniz (=) variant; use bigOpM_weak_hom

Leibniz (=) variant; use bigOpM_hom

Not needed

Merged into bigOpM_eq

Use bigOpM_dist

Use bigOpM_eq

Not needed

Not needed

Leibniz (=) variant; use BigOpS.hom_weak

Leibniz (=) variant; use BigOpS.hom

Not needed

Merged into bigOpS_eq

Use bigOpS_dist

Use bigOpS_eq

Not needed

Implicit in the type of `Completion.unit`.

OFE equality is Leibniz equality.

Implicit in the type of `Completion.map`.

Non needed.

Implicit in the type of `Completion.complete`.

OFE equality is Leibniz equality.

Derived from nonexpansivity

Use the CMRA type class.

OFE is Leibniz; use equality

Use CMRA instance

Use CMRA instance

Use CMRA instance

Use CMRA instance

Use CMRA instance

OFE is Leibniz; use equality

Derived from nonexpansivity

Use the CMRA.op field.

Use the CMRA.pcore field.

Bundled record of RA laws; Lean passes them as arguments to `CMRA.ofDiscrete`.

Lean uses the UCMRA type class directly; mixin/bundle separation is unnecessary.

Lean uses the UCMRA.unit field; no separate class needed.

Use the CMRA.Valid field.

Use the CMRA.ValidN field.

OFE is Leibniz; use equality

Derived from core_ne

Reflexivity is incN_refl; transitivity is the Trans instance

OFE is Leibniz; use equality

Reflexivity is inc_refl; transitivity is the Trans instance

OFE is Leibniz; use equality

Not needed.

Use cmra_mono

Use cmra_monoN

OFE is Leibniz; use equality

Not needed.

Derived from nonexpansivity

OFE is Leibniz; use equality

OFE is Leibniz; use equality

OFE is Leibniz; use equality

Use CMRA + IsTotal

Use `transpAp`

Use `OFE.transpAp_pcore_mp`

No counterpart; see the `transpAp` family

No counterpart; see the `transpAp` family

Use `OFE.transpAp_eqv_mp`

Use `OFE.transpAp_op_mp`

OFE is Leibniz; use equality

Use `transpAp` with `Eq.trans`

Use `OFE.transpAp_validN_mp`/`OFE.validN_transpAp_mp` with `CMRA.valid_iff_validN`

Use `OFE.transpAp_validN_mp` and its converse `OFE.validN_transpAp_mp`

OFE is Leibniz; use equality

OFE is Leibniz; use equality

Use CMRA instance

Use CMRA instance

Use CMRA instance

Use UCMRA instance

Use UCMRA instance

Use CMRA instance

Use CMRA instance

Use CMRA instance

OFE is Leibniz; use equality

Provided by `URFunctor.toRFunctor` from `urFunctorOptionOF`.

Provided by `URFunctorContractive.toRFunctorContractive` from `urFunctorContractiveOptionOF`.

Use CMRA instance

Use CMRA instance

Use UCMRA instance

Use UCMRA instance

Use CMRA instance

Use CMRA instance

Use CMRA instance

Use CMRA instance

Use UCMRA instance

Use UCMRA instance

Use CMRA instance

Use CMRA instance

Just apply the underlying `OFunctorPre`

Folded into Lean's UCMRA extends CMRA.

Folded into Lean's UCMRA → OFE.

Subsumed by empty_cancelable

Subsumed by unit_CoreId

Use CMRA instance

Use CMRA instance

Use UCMRA instance

Use UCMRA instance

Use CMRA instance

Use CMRA instance

Just apply the underlying `OFunctorPre`

Provided by the generic `CMRA.Discrete (LeibnizSet S)` instance.

Provided by `CMRA.Discrete (DisjointLeibnizSet S)`.

Provided by the `CMRA (DisjointLeibnizSet S)` instance.

Provided by the `CMRA (DisjointLeibnizSet S)` instance.

Provided by the `CMRA (DisjointLeibnizSet S)` instance.

Provided by the `UCMRA (DisjointLeibnizSet S)` instance.

Provided by the `UCMRA (DisjointLeibnizSet S)` instance.

Provided by the `CMRA (DisjointLeibnizSet S)` instance.

Provided by the `CMRA (LeibnizSet S)` instance.

Provided by the `CMRA (LeibnizSet S)` instance.

Provided by the `CMRA (LeibnizSet S)` instance.

Provided by the `UCMRA (LeibnizSet S)` instance.

Provided by the `UCMRA (LeibnizSet S)` instance.

Provided by the `CMRA (LeibnizSet S)` instance.

Use OFE.iso + Inhabited + COFE

Inference succeeds automatically via `instA`/`instA'`

Not needed

Inlined in embed

Lean's Tower.embed is already a bundled non-expansive map

Implicit in embed

Not needed

Inlined in Tower.embed_up

Implicit in the OFE.Iso structure

Not needed

Inlined in Tower.embed, as its well-definedness obligation

Inlined in Tower.embed

Use `Fix F` with Inhabited + COFE instances and Fix.iso

Use NonExpansive instance

Use IsCOFE instance

Use IsCOFE instance

Included in OFE (Tower F) instance

Included in OFE (Tower F) instance

Implicit in Lean's Inhabited (Tower F) instance

Not needed

Implicit in the OFE.Iso structure

Derivable using NonExpansive.eqv

Derivable using NonExpansive.eqv

Use Csum type with typeclass inference

Included in IsCOFE instance

OFE is Leibniz; use equality

Not needed

Not needed

Use CMRA instance

Use CMRA instance

Use CMRA instance

Use CMRA instance

std++ `Maybe` class; pattern match instead

std++ `Maybe` class; pattern match instead

Not needed

Not needed

Use DFrac type with typeclass inference

Use CMRA instance

Use CMRA instance

Not needed

Use CMRA instance

Derivable using NonExpansive.eqv

Derivable using UCMRA

Not needed

Derivable using NonExpansive.eqv

Derivable using NonExpansive.eqv

Part of OFE instance

Part of UCMRA instance

Part of OFE instance

Not needed

Use CMRA core instead

Not needed

Definitional unfolding of ValidN

Definitional unfolding of Valid

OFE/CMRA are built directly, not via an isomorphism

OFE/CMRA are built directly, not via an isomorphism

Derivable from NonExpansive.eqv

Not needed

OFE is Leibniz; use equality

Not needed

Not needed

Use CMRA instance

Use CMRA instance

Use CMRA instance

Use CMRA instance

std++ `Maybe` class; pattern match instead

Use CMRA instance

Use CMRA instance

Use CMRA instance

Use CMRA instance

Use the NonExpansive instance instead.

Use NonExpansive instance instead.

OFE is Leibniz; use equality

Found by typeclass inference

Found by typeclass inference

Included in the OFE instance

Provided by the `CMRA (LeibnizMultiSet MS)` instance.

Provided by the `CMRA (LeibnizMultiSet MS)` instance.

Provided by the `CMRA (LeibnizMultiSet MS)` instance.

Provided by the `UCMRA (LeibnizMultiSet MS)` instance.

Provided by the `UCMRA (LeibnizMultiSet MS)` instance.

Provided by the `CMRA (LeibnizMultiSet MS)` instance.

Provided by the `CMRA (LeibnizMultiSet MS)` instance.

Use the constructor injectivity lemma DisjointLeibnizSet.valid.inj

Use `[LawfulSet S A] → LeibnizSet S` and its `COFE` instance.

Use `[LawfulSet S A] → LeibnizSet S` and its `CMRA` instance.

Use `[LawfulSet S A] → LeibnizSet S` and its `UCMRA` instance.

Provided by the generic `CMRA.Discrete (LeibnizSet S)` instance.

Use `[LawfulSet S A] → DisjointLeibnizSet S`.

Use `[LawfulSet S A] → DisjointLeibnizSet S` and its `COFE` instance.

Use `[LawfulSet S A] → DisjointLeibnizSet S` and its `CMRA` instance.

Use `[LawfulSet S A] → DisjointLeibnizSet S` and its `UCMRA` instance.

Provided by `CMRA.Discrete (DisjointLeibnizSet S)`.

Provided by the `CMRA (DisjointLeibnizSet S)` instance.

Provided by the `CMRA (DisjointLeibnizSet S)` instance.

Provided by the `CMRA (DisjointLeibnizSet S)` instance.

Provided by the `UCMRA (DisjointLeibnizSet S)` instance.

Provided by the `UCMRA (DisjointLeibnizSet S)` instance.

Provided by the `CMRA (DisjointLeibnizSet S)` instance.

Provided by the `CMRA (LeibnizSet S)` instance.

Provided by the `CMRA (LeibnizSet S)` instance.

Provided by the `CMRA (LeibnizSet S)` instance.

Provided by the `UCMRA (LeibnizSet S)` instance.

Provided by the `UCMRA (LeibnizSet S)` instance.

Provided by the `CMRA (LeibnizSet S)` instance.

std++ `SetUnfold` instance for `set_solver`; use DisjointLeibnizSet.included_iff_subset

std++ `SetUnfold` instance for `set_solver`; use DisjointLeibnizSet.valid_op_iff_disj

std++ `SetUnfold` instance for `set_solver`; no counterpart in Lean

std++ `SetUnfold` instance for `set_solver`; use LeibnizSet.included_iff_subset

Found by typeclass inference

Use included

Use op_valid

Use included

Use op_valid

Derivable from mk_ne with NonExpansive.eqv

Found by typeclass inference

Found by typeclass inference

Use agree

Derivable from auth_ne with NonExpansive.eqv

Derivable from frag_ne with NonExpansive.eqv