def Iris.Std.rwRule' : Lean.ParserDescr

Rewrite rules for rw' have the same structure as for rw, except they allow an additional ! prefix to indicate that a rewrite rule should be used as often as possible.

Equations

• One or more equations did not get rendered due to their size.

inductive Iris.Std.RewriteModifier : Type

Modifier for a rewrite rule to indicate how often is should be used.

• single : RewriteModifier
• all : RewriteModifier

inductive Iris.Std.RewriteDirection : Type

Rewrite direction of a rwRule.

• forward : RewriteDirection
• reverse : RewriteDirection

opaque Iris.Std.monoRulesExt : Lean.SimplePersistentEnvExtension Lean.Name Lean.NameSet

Register an environment extension to hold all operator destruction rules.

def Iris.Std.«tacticRw'[_,,]» : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.