def Duper.occursInLambdaNotDirectlyBelowQuantifier (c : MClause) (t : Lean.Expr) : Bool

Note: This function currently excludes lambdas that appear in forallE, lam, or letE types.

Equations

• Duper.occursInLambdaNotDirectlyBelowQuantifier c t = Duper.MClause.fold (fun (b : Bool) (e : Lean.Expr) => b || Duper.occursInLambdaNotDirectlyBelowQuantifier.visit t e false false) false c

@[specialize #[]]

def Duper.occursInLambdaNotDirectlyBelowQuantifier.visit (t e : Lean.Expr) (directlyBelowQuantifier inLambda : Bool) : Bool

Equations

• One or more equations did not get rendered due to their size.
• Duper.occursInLambdaNotDirectlyBelowQuantifier.visit t e directlyBelowQuantifier inLambda = if (inLambda && e == t) = true then true else false

def Duper.occursInArgumentOfAppliedVariable (c : MClause) (t : Lean.Expr) : Bool

Equations

• Duper.occursInArgumentOfAppliedVariable c t = Duper.MClause.fold (fun (b : Bool) (e : Lean.Expr) => b || Duper.occursInArgumentOfAppliedVariable.visit t e false) false c

@[specialize #[]]

def Duper.occursInArgumentOfAppliedVariable.visit (t e : Lean.Expr) (inArgumentOfAppliedVariable : Bool) : Bool

Equations

• One or more equations did not get rendered due to their size.
• Duper.occursInArgumentOfAppliedVariable.visit t e inArgumentOfAppliedVariable = if (inArgumentOfAppliedVariable && e == t) = true then true else false

def Duper.isDeep (c : MClause) (t : Lean.Expr) : Bool

Returns true if t is an mvar that occurs deeply in MClause c.

A variable occurs deeply in an mclause c if it occurs inside an argument of an applied variable or inside a λ-expression that is not directly below a quantifier.

Equations

• Duper.isDeep c t = (t.isMVar' && (Duper.occursInArgumentOfAppliedVariable c t || Duper.occursInLambdaNotDirectlyBelowQuantifier c t))

def Duper.isFluidOrDeep (c : MClause) (t : Lean.Expr) : Bool

A syntactic overapproximation of fluid or deep terms

Equations

• Duper.isFluidOrDeep c t = (Duper.Order.isFluid t || Duper.isDeep c t)