opaque Duper.reduceInstances : Lean.Option Bool

Note: This option should never be enabled if Duper will later call the monomorphization procedure because attempting to reduce typeclass instances can interfere with monomorphization. It also does not appear to provide observable benefit even when the monomorphization procedure is not being called, so it is currently disabled at all times. The option is just left around (rather than deleted entirely) for testing purposes.

def Duper.getReduceInstances (opts : Lean.Options) : Bool

Equations

• Duper.getReduceInstances opts = Lean.Option.get opts Duper.reduceInstances

def Duper.getReduceInstancesM : Lean.CoreM Bool

Equations

• Duper.getReduceInstancesM = do let opts ← Lean.getOptions pure (Duper.getReduceInstances opts)

def Duper.preprocessFact (fact : Lean.Expr) : Lean.MetaM Lean.Expr

This function is expensive and should only be used in preprocessing

Equations

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

partial def Duper.etaLong (e : Lean.Expr) : Lean.MetaM Lean.Expr

Eta-expand a beta-reduced expression. This function is currently unused

partial def Duper.etaLong.mkForallFVarsEtaLong (xs : Array Lean.Expr) (b : Lean.Expr) : Lean.MetaM Lean.Expr

partial def Duper.etaLong.mkLambdaFVarsEtaLong (xs : Array Lean.Expr) (b : Lean.Expr) : Lean.MetaM Lean.Expr

def Duper.etaReduce (e : Lean.Expr) : Lean.MetaM Lean.Expr

Applies eta reduction to e and all of its subexpressions TODO: Make sure that when calling this function from other files, the term supplied to it does not contain loose bound variables.

Equations

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

def Duper.betaEtaReduceInstMVars (e : Lean.Expr) : Lean.MetaM Lean.Expr

Instantiates mvars then applies beta and eta reduction exhaustively.

Equations

• Duper.betaEtaReduceInstMVars e = do let e ← Lean.instantiateMVars e let e ← liftM (Lean.Core.betaReduce e) Duper.etaReduce e

def Duper.betaEtaReduce (e : Lean.Expr) : Lean.MetaM Lean.Expr

Applies beta and eta reduction exhaustively

Equations

• Duper.betaEtaReduce e = do let e ← liftM (Lean.Core.betaReduce e) Duper.etaReduce e