opaque Duper.duper.printPortfolioInstance : Lean.Option Bool

opaque Duper.duper.throwPortfolioErrors : Lean.Option Bool

opaque Duper.duper.collectDatatypes : Lean.Option Bool

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

Equations

• Duper.getPrintPortfolioInstance opts = Lean.Option.get opts Duper.duper.printPortfolioInstance

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

Equations

• Duper.getThrowPortfolioErrors opts = Lean.Option.get opts Duper.duper.throwPortfolioErrors

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

Equations

• Duper.getCollectDataTypes opts = Lean.Option.get opts Duper.duper.collectDatatypes

def Duper.getPrintPortfolioInstanceM : Lean.CoreM Bool

Equations

• Duper.getPrintPortfolioInstanceM = do let opts ← Lean.getOptions pure (Duper.getPrintPortfolioInstance opts)

def Duper.getThrowPortfolioErrorsM : Lean.CoreM Bool

Equations

• Duper.getThrowPortfolioErrorsM = do let opts ← Lean.getOptions pure (Duper.getThrowPortfolioErrors opts)

def Duper.getCollectDataTypesM : Lean.CoreM Bool

Equations

• Duper.getCollectDataTypesM = do let opts ← Lean.getOptions pure (Duper.getCollectDataTypes opts)

def Duper.Duper.bool_lit.quot : Lean.ParserDescr

Equations

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

def Lean.Parser.Category.Duper.bool_lit : Category

Equations

• Lean.Parser.Category.Duper.bool_lit = { }

def Duper.bool_litTrue : Lean.ParserDescr

Equations

• Duper.bool_litTrue = Lean.ParserDescr.node `Duper.bool_litTrue 1024 (Lean.ParserDescr.nonReservedSymbol "true" false)

def Duper.bool_litFalse : Lean.ParserDescr

Equations

• Duper.bool_litFalse = Lean.ParserDescr.node `Duper.bool_litFalse 1024 (Lean.ParserDescr.nonReservedSymbol "false" false)

def Duper.elabBoolLit {m : Type → Type} [Monad m] [Lean.MonadError m] (stx : Lean.TSyntax `Duper.bool_lit) : m Bool

Equations

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

def Duper.boolToBoolLit {m : Type → Type} [Monad m] [Lean.MonadQuotation m] (b : Bool) : m (Lean.TSyntax `Duper.bool_lit)

Equations

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

def Lean.Parser.Category.Duper.preprocessing_option : Category

Equations

• Lean.Parser.Category.Duper.preprocessing_option = { }

def Duper.Duper.preprocessing_option.quot : Lean.ParserDescr

Equations

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

def Duper.preprocessing_optionFull : Lean.ParserDescr

Equations

• Duper.preprocessing_optionFull = Lean.ParserDescr.node `Duper.preprocessing_optionFull 1024 (Lean.ParserDescr.nonReservedSymbol "full" false)

def Duper.preprocessing_optionMonomorphization : Lean.ParserDescr

Equations

• Duper.preprocessing_optionMonomorphization = Lean.ParserDescr.node `Duper.preprocessing_optionMonomorphization 1024 (Lean.ParserDescr.nonReservedSymbol "monomorphization" false)

def Duper.preprocessing_optionNo_preprocessing : Lean.ParserDescr

Equations

• Duper.preprocessing_optionNo_preprocessing = Lean.ParserDescr.node `Duper.preprocessing_optionNo_preprocessing 1024 (Lean.ParserDescr.nonReservedSymbol "no_preprocessing" false)

inductive Duper.PreprocessingOption : Type

• FullPreprocessing : PreprocessingOption
• Monomorphization : PreprocessingOption
• NoPreprocessing : PreprocessingOption

instance Duper.instDecidableEqPreprocessingOption : DecidableEq PreprocessingOption

Equations

• Duper.instDecidableEqPreprocessingOption x✝ y✝ = if h : x✝.toCtorIdx = y✝.toCtorIdx then isTrue ⋯ else isFalse ⋯

def Duper.elabPreprocessingOption {m : Type → Type} [Monad m] [Lean.MonadError m] (stx : Lean.TSyntax `Duper.preprocessing_option) : m PreprocessingOption

Equations

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

def Duper.preprocessingOptionToStx {m : Type → Type} [Monad m] [Lean.MonadQuotation m] (o : PreprocessingOption) : m (Lean.TSyntax `Duper.preprocessing_option)

Equations

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

def Duper.Duper.configOption.quot : Lean.ParserDescr

Equations

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

def Lean.Parser.Category.Duper.configOption : Category

Equations

• Lean.Parser.Category.Duper.configOption = { }

def Duper.«configOptionPortfolioMode:=_» : Lean.ParserDescr

Equations

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

def Duper.«configOptionPortfolioInstance:=_» : Lean.ParserDescr

Equations

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

def Duper.«configOptionInhabitationReasoning:=_» : Lean.ParserDescr

Equations

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

def Duper.«configOptionPreprocessing:=_» : Lean.ParserDescr

Equations

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

def Duper.«configOptionIncludeExpensiveRules:=_» : Lean.ParserDescr

Equations

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

def Duper.«configOptionSelFunction:=_» : Lean.ParserDescr

Equations

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

structure Duper.ConfigurationOptions : Type

• portfolioMode : Bool
• portfolioInstance : Option Nat
• inhabitationReasoning : Option Bool
• preprocessing : Option PreprocessingOption
• includeExpensiveRules : Option Bool
• selFunction : Option Nat

def Duper.duperStar : Lean.ParserDescr

Equations

• Duper.duperStar = Lean.ParserDescr.nodeWithAntiquot "duperStar" `Duper.duperStar (Lean.ParserDescr.symbol "*")

def Duper.duper : Lean.ParserDescr

duper [facts] {options} is a terminal tactic that uses an automatic theorem prover to attempt to solve the current main goal.

The facts supplied to duper are separated by commas and can include:

• Hypotheses (of type Prop) from the local context
• External lemmas
• The symbol * to indicate that duper should consider all proofs in the current local context

Duper can also optionally receive a second list of facts (extra facts) that are to be added but not included in the set of support.

By default, duper will call multiple instances of itself with different option configurations in an attempt to find the option configuration that is best suited for the current problem. This behavior can be changed by including the option portfolioMode := false in the comma separated options list. Running duper with portfolioMode enabled means that each instance of duper will be given less time to run. To increase the amount of time allocated to duper, use set_option maxHeartbeats <num> (setting <num> to 3 times the default value will ensure that each duper instance is given as much time as it would receive if run with portfolioMode disabled).

The variant duper? will call duper and, if a proof is found, return a Try this suggestion that will call duper using just the option configuration that succeeded in finding a proof. If the suggestion is used, then on all subsequent compilations, only the version of duper that succeeded will be called.

Additional options that can be included in the options list include:

• portfolioInstance: Can be set to a natural number from 0 to 24 and corresponds to an exact set of options by which duper can be called.
• preprocessing: Can be set to full, monomorphization, or no_preprocessing.
• inhabitationReasoning: Can be set to true or false.
• includeExpensiveRules: Can be set to true or false.

For a more complete referenceon duper (including fuller descriptions of the various options), see its README

Equations

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

def Duper.duperTrace : Lean.ParserDescr

duper [facts] {options} is a terminal tactic that uses an automatic theorem prover to attempt to solve the current main goal.

The facts supplied to duper are separated by commas and can include:

• Hypotheses (of type Prop) from the local context
• External lemmas
• The symbol * to indicate that duper should consider all proofs in the current local context

Duper can also optionally receive a second list of facts (extra facts) that are to be added but not included in the set of support.

By default, duper will call multiple instances of itself with different option configurations in an attempt to find the option configuration that is best suited for the current problem. This behavior can be changed by including the option portfolioMode := false in the comma separated options list. Running duper with portfolioMode enabled means that each instance of duper will be given less time to run. To increase the amount of time allocated to duper, use set_option maxHeartbeats <num> (setting <num> to 3 times the default value will ensure that each duper instance is given as much time as it would receive if run with portfolioMode disabled).

The variant duper? will call duper and, if a proof is found, return a Try this suggestion that will call duper using just the option configuration that succeeded in finding a proof. If the suggestion is used, then on all subsequent compilations, only the version of duper that succeeded will be called.

Additional options that can be included in the options list include:

• portfolioInstance: Can be set to a natural number from 0 to 24 and corresponds to an exact set of options by which duper can be called.
• preprocessing: Can be set to full, monomorphization, or no_preprocessing.
• inhabitationReasoning: Can be set to true or false.
• includeExpensiveRules: Can be set to true or false.

For a more complete referenceon duper (including fuller descriptions of the various options), see its README

Equations

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

def Duper.portfolioInstanceToConfigOptionStx {m : Type → Type} [Monad m] [Lean.MonadError m] [Lean.MonadQuotation m] (n : Nat) : m (Lean.TSyntax `Duper.configOption)

If n is a Nat that corresponds to one of Duper's portfolio instances, then portfolioInstanceToConfigOptionStx n returns the syntax object corresponding to portfolioInstance := n. This is necessary so that duper? can produce its suggestion.

def Duper.selFunctionNumToConfigOptionStx {m : Type → Type} [Monad m] [Lean.MonadError m] [Lean.MonadQuotation m] (n : Nat) : m (Lean.TSyntax `Duper.configOption)

If n is a Nat that corresponds to one of Duper's selection functions, then selFunctionNumToConfigOptionStx n returns the syntax object corresponding to selFunction := n. This is necessary so that duper? can produce its suggestion.

Equations

• One or more equations did not get rendered due to their size.
• Duper.selFunctionNumToConfigOptionStx n = Lean.throwError (Lean.toMessageData "Invalid selFunction option")

def Duper.mkDuperCallSuggestion (duperStxRef origSpan : Lean.Syntax) (facts : Lean.Syntax.TSepArray `term ",") (extraFacts : Option (Lean.Syntax.TSepArray `term ",")) (withDuperStar : Bool) (portfolioInstance : Nat) (inhabitationReasoning : Option Bool := none) (preprocessing : Option PreprocessingOption := none) (includeExpensiveRules : Option Bool := none) (selFunction : Option Nat := none) : Lean.MetaM Unit

Constructs and suggests the syntax for a duper call, for use with duper? If a portfolioInstance other than 0 is specified, then the returned tactic will only specify that instance (since it is all that is necessary). If the portfolioInstance specified is 0, then the returned tactic will use all of the optional arguments to construct the suggested syntax.

Equations

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

def Duper.withoutModifyingCoreEnv {α : Type} (m : Lean.MetaM α) : Lean.MetaM α

We save the CoreM state. This is because we will add a constant skolemSorry to the environment to support skolem constants with universe levels. We want to erase this constant after the saturation procedure ends

Equations

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

axiom Duper.skSorryAx {α : Sort u} : α

skSorryAx has essentially the same type as sorryAx, but does not trigger a sorry warning in Lean.addAndCompile. We want to deliberately bypass the warning in Lean.addAndCompile because the skolemSorry constant that Duper adds to the environment is only temporary and will be removed from the actual proof that should be checked by the kernel.

def Duper.addSkolemSorry : Lean.CoreM Lean.Name

Add the constant skolemSorry to the environment and add suitable postfix to avoid name conflict.

Equations

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

def Duper.unfoldDefinitions (formulas : List (Lean.Expr × Lean.Expr × Array Lean.Name × Bool × Bool)) : Lean.MetaM (List (Lean.Expr × Lean.Expr × Array Lean.Name × Bool × Bool))

Equations

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

def Duper.printSaturation (state : ProverM.State) : Lean.MetaM Unit

Equations

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

def Duper.formulasToMessageData : Lean.Expr × Lean.Expr × Array Lean.Name × Bool × Bool → Lean.MessageData

Equations

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

def Duper.runDuper (formulas extraFormulas : List (Lean.Expr × Lean.Expr × Array Lean.Name × Bool)) (instanceMaxHeartbeats : Nat) : Lean.MetaM Lean.Expr

Entry point for calling a single instance of duper using the options determined by (← getOptions).

Formulas should consist of lemmas supplied by the user (to see how to obtain formulas from duper's input syntax, see collectAssumptions). InstanceMaxHeartbeats should indicate how many heartbeats duper should run for before timing out (if instanceMaxHeartbeats is set to 0, then duper will run until it is timed out by the Core maxHeartbeats option). If Duper succeeds in deriving a contradiction and constructing a proof for it, then runDuper returns that proof as an expression. Otherwise, Duper will throw an error.

Equations

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

partial def Duper.getLeavesFromDTr (t : Auto.DTr) : Array String

def Duper.formulasToAutoLemmas (formulas : List (Lean.Expr × Lean.Expr × Array Lean.Name × Bool × Option Lean.Term)) (includeInSetOfSupport : Bool) : Lean.MetaM (Array Auto.Lemma)

Converts formulas/lemmas from the format used by Duper to the format used by Auto. Duper uses Auto's deriv DTr to keep track of isFromGoal and optional syntax information through the monomorphization procedure.

Equations

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

def Duper.formulasWithStringsToAutoLemmas (formulas : List (Lean.Expr × Lean.Expr × Array Lean.Name × Bool × Option String)) (includeInSetOfSupport : Bool) : Lean.MetaM (Array Auto.Lemma)

Like formulasToAutoLemmas, but the stxOption is a string instead of a term.

Equations

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

def Duper.derivInfo (lem : Auto.Lemma) : Bool × Bool

Determines whether lem's deriv info indicates that lem is part of the goal and should be included in the set of support. Note that derivInfo only works on lemmas generated from formulasToAutoLemmas or formulasWithStringsToAutoLemmas. In cases where the lemma was not generated from formulasToAutoLemmas, derivInfo defaults to indicating that both isFromGoal and includeInSetOfSupport are true.

Equations

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

def Duper.autoLemmasToFormulas (lemmas : Array Auto.Lemma) : Lean.MetaM (List (Lean.Expr × Lean.Expr × Array Lean.Name × Bool) × List (Lean.Expr × Lean.Expr × Array Lean.Name × Bool))

Converts formulas/lemmas from the format used by Auto to the format used by Duper.

Equations

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

def Duper.runDuperInstanceWithMonomorphization (formulas extraFormulas : List (Lean.Expr × Lean.Expr × Array Lean.Name × Bool × Option Lean.Term)) (instanceMaxHeartbeats : Nat) (inst : List (Lean.Expr × Lean.Expr × Array Lean.Name × Bool) → List (Lean.Expr × Lean.Expr × Array Lean.Name × Bool) → Nat → Lean.MetaM Lean.Expr) : Lean.MetaM Lean.Expr

Given formulas, instanceMaxHeartbeats, and an instance of Duper inst, runs inst with monomorphization preprocessing.

Equations

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

def Duper.runDuperInstanceWithFullPreprocessing (formulas extraFormulas : List (Lean.Expr × Lean.Expr × Array Lean.Name × Bool × Option Lean.Term)) (declName? : Option Lean.Name) (instanceMaxHeartbeats : Nat) (inst : List (Lean.Expr × Lean.Expr × Array Lean.Name × Bool) → List (Lean.Expr × Lean.Expr × Array Lean.Name × Bool) → Nat → Lean.MetaM Lean.Expr) : Lean.MetaM Lean.Expr

Given formulas, instanceMaxHeartbeats, declName? and an instance of Duper inst, runs inst with all of Auto's preprocessing (monomorphization, skolemization, definition unfolding, exhaustive function extensionality rewrites, and BitVec simplicfication).

Equations

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

def Duper.mkDuperInstance (formulas extraFormulas : List (Lean.Expr × Lean.Expr × Array Lean.Name × Bool × Option Lean.Term)) (declName? : Option Lean.Name) (instanceMaxHeartbeats : Nat) (inhabitationReasoning : Option Bool) (preprocessing : Option PreprocessingOption) (includeExpensiveRules : Option Bool) (selFunction : Option Nat) : Lean.MetaM Lean.Expr

mkDuperInstance is called by each runDuperInstanceN function to construct the desired Duper instance. Additionally, if a user invokes portfolio instance 0 (which is the special instance reserved for allowing the user to manually construct an instance with their own configuration options), then this function will be called directly.

Equations

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

def Duper.runDuperInstance1 (formulas extraFormulas : List (Lean.Expr × Lean.Expr × Array Lean.Name × Bool × Option Lean.Term)) (declName? : Option Lean.Name) (instanceMaxHeartbeats : Nat) : Lean.MetaM Lean.Expr

First instance called by portfolio mode. Has the following options:

• preprocessing = full
• inhabitationReasoning = false
• selFunction = 4 (which corresponds to Zipperposition's default selection function)
• includeExpensiveRules = false

Equations

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

def Duper.runDuperInstance2 (formulas extraFormulas : List (Lean.Expr × Lean.Expr × Array Lean.Name × Bool × Option Lean.Term)) (declName? : Option Lean.Name) (instanceMaxHeartbeats : Nat) : Lean.MetaM Lean.Expr

Same as duper instance 1 except inhabitation reasoning is enabled. Has the following options:

• preprocessing = full
• inhabitationReasoning = true
• selFunction = 4 (which corresponds to Zipperposition's default selection function)
• includeExpensiveRules = false

Equations

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

def Duper.runDuperInstance3 (formulas extraFormulas : List (Lean.Expr × Lean.Expr × Array Lean.Name × Bool × Option Lean.Term)) (declName? : Option Lean.Name) (instanceMaxHeartbeats : Nat) : Lean.MetaM Lean.Expr

Second instance called by portfolio mode. Has the following options:

• preprocessing = full
• inhabitationReasoning = false
• selFunction = 11 (which corresponds to E's SelectMaxLComplexAvoidPosPred and Zipperposition's e_sel)
• includeExpensiveRules = true

Equations

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

def Duper.runDuperInstance4 (formulas extraFormulas : List (Lean.Expr × Lean.Expr × Array Lean.Name × Bool × Option Lean.Term)) (declName? : Option Lean.Name) (instanceMaxHeartbeats : Nat) : Lean.MetaM Lean.Expr

Same as duper instance 3 except inhabitation reasoning is enabled. Has the following options:

• preprocessing = full
• inhabitationReasoning = true
• selFunction = 11 (which corresponds to E's SelectMaxLComplexAvoidPosPred and Zipperposition's e_sel)
• includeExpensiveRules = true

Equations

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

def Duper.runDuperInstance5 (formulas extraFormulas : List (Lean.Expr × Lean.Expr × Array Lean.Name × Bool × Option Lean.Term)) (declName? : Option Lean.Name) (instanceMaxHeartbeats : Nat) : Lean.MetaM Lean.Expr

Third instance called by portfolio mode. Has the following options:

• preprocessing = full
• inhabitationReasoning = false
• selFunction = 13 (which corresponds to E's SelectComplexG and Zipperposition's e_sel3)
• includeExpensiveRules = false

Equations

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

def Duper.runDuperInstance6 (formulas extraFormulas : List (Lean.Expr × Lean.Expr × Array Lean.Name × Bool × Option Lean.Term)) (declName? : Option Lean.Name) (instanceMaxHeartbeats : Nat) : Lean.MetaM Lean.Expr

Same as duper instance 5 except inhabitation reasoning is enabled. Has the following options:

• preprocessing = full
• inhabitationReasoning = true
• selFunction = 13 (which corresponds to E's SelectComplexG and Zipperposition's e_sel3)
• includeExpensiveRules = false

Equations

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

def Duper.runDuperInstance7 (formulas extraFormulas : List (Lean.Expr × Lean.Expr × Array Lean.Name × Bool × Option Lean.Term)) (declName? : Option Lean.Name) (instanceMaxHeartbeats : Nat) : Lean.MetaM Lean.Expr

Fourth instance called by portfolio mode. Has the following options:

• preprocessing = no_preprocessing
• inhabitationReasoning = true
• selFunction = 2 (NoSelection)
• includeExpensiveRules = true

Equations

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

def Duper.runDuperInstance8 (formulas extraFormulas : List (Lean.Expr × Lean.Expr × Array Lean.Name × Bool × Option Lean.Term)) (declName? : Option Lean.Name) (instanceMaxHeartbeats : Nat) : Lean.MetaM Lean.Expr

Same as duper instance 7 except inhabitation reasoning is disabled. Has the following options:

• preprocessing = no_preprocessing
• inhabitationReasoning = false
• selFunction = 2 (NoSelection)
• includeExpensiveRules = true

Equations

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

def Duper.runDuperInstance9 (formulas extraFormulas : List (Lean.Expr × Lean.Expr × Array Lean.Name × Bool × Option Lean.Term)) (declName? : Option Lean.Name) (instanceMaxHeartbeats : Nat) : Lean.MetaM Lean.Expr

Same as duper instance 1 except preprocessing is disabled. Has the following options:

• preprocessing = no_preprocessing
• inhabitationReasoning = false
• selFunction = 4 (which corresponds to Zipperposition's default selection function)
• includeExpensiveRules = false

Equations

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

def Duper.runDuperInstance10 (formulas extraFormulas : List (Lean.Expr × Lean.Expr × Array Lean.Name × Bool × Option Lean.Term)) (declName? : Option Lean.Name) (instanceMaxHeartbeats : Nat) : Lean.MetaM Lean.Expr

Same as duper instance 2 except preprocessing is disabled. Has the following options:

• preprocessing = no_preprocessing
• inhabitationReasoning = true
• selFunction = 4 (which corresponds to Zipperposition's default selection function)
• includeExpensiveRules = false

Equations

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

def Duper.runDuperInstance11 (formulas extraFormulas : List (Lean.Expr × Lean.Expr × Array Lean.Name × Bool × Option Lean.Term)) (declName? : Option Lean.Name) (instanceMaxHeartbeats : Nat) : Lean.MetaM Lean.Expr

Same as duper instance 3 except preprocessing is disabled. Has the following options:

• preprocessing = no_preprocessing
• inhabitationReasoning = false
• selFunction = 11 (which corresponds to E's SelectMaxLComplexAvoidPosPred and Zipperposition's e_sel)
• includeExpensiveRules = true

Equations

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

def Duper.runDuperInstance12 (formulas extraFormulas : List (Lean.Expr × Lean.Expr × Array Lean.Name × Bool × Option Lean.Term)) (declName? : Option Lean.Name) (instanceMaxHeartbeats : Nat) : Lean.MetaM Lean.Expr

Same as duper instance 4 except preprocessing is disabled. Has the following options:

• preprocessing = no_preprocessing
• inhabitationReasoning = true
• selFunction = 11 (which corresponds to E's SelectMaxLComplexAvoidPosPred and Zipperposition's e_sel)
• includeExpensiveRules = true

Equations

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

def Duper.runDuperInstance13 (formulas extraFormulas : List (Lean.Expr × Lean.Expr × Array Lean.Name × Bool × Option Lean.Term)) (declName? : Option Lean.Name) (instanceMaxHeartbeats : Nat) : Lean.MetaM Lean.Expr

Same as duper instance 5 except preprocessing is disabled. Has the following options:

• preprocessing = no_preprocessing
• inhabitationReasoning = false
• selFunction = 13 (which corresponds to E's SelectComplexG and Zipperposition's e_sel3)
• includeExpensiveRules = false

Equations

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

def Duper.runDuperInstance14 (formulas extraFormulas : List (Lean.Expr × Lean.Expr × Array Lean.Name × Bool × Option Lean.Term)) (declName? : Option Lean.Name) (instanceMaxHeartbeats : Nat) : Lean.MetaM Lean.Expr

Same as duper instance 6 except preprocessing is disabled. Has the following options:

• preprocessing = no_preprocessing
• inhabitationReasoning = true
• selFunction = 13 (which corresponds to E's SelectComplexG and Zipperposition's e_sel3)
• includeExpensiveRules = false

Equations

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

def Duper.runDuperInstance15 (formulas extraFormulas : List (Lean.Expr × Lean.Expr × Array Lean.Name × Bool × Option Lean.Term)) (declName? : Option Lean.Name) (instanceMaxHeartbeats : Nat) : Lean.MetaM Lean.Expr

Same as duper instance 7 except preprocessing is enabled. Has the following options:

• preprocessing = full
• inhabitationReasoning = true
• selFunction = 2 (NoSelection)
• includeExpensiveRules = true

Equations

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

def Duper.runDuperInstance16 (formulas extraFormulas : List (Lean.Expr × Lean.Expr × Array Lean.Name × Bool × Option Lean.Term)) (declName? : Option Lean.Name) (instanceMaxHeartbeats : Nat) : Lean.MetaM Lean.Expr

Same as duper instance 8 except preprocessing is enabled. Has the following options:

• preprocessing = full
• inhabitationReasoning = false
• selFunction = 2 (NoSelection)
• includeExpensiveRules = true

Equations

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

def Duper.runDuperInstance17 (formulas extraFormulas : List (Lean.Expr × Lean.Expr × Array Lean.Name × Bool × Option Lean.Term)) (declName? : Option Lean.Name) (instanceMaxHeartbeats : Nat) : Lean.MetaM Lean.Expr

Same as duper instance 1 except preprocessing is set to monomorphization only. Has the following options:

• preprocessing = monomorphization
• inhabitationReasoning = false
• selFunction = 4 (which corresponds to Zipperposition's default selection function)
• includeExpensiveRules = false

Equations

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

def Duper.runDuperInstance18 (formulas extraFormulas : List (Lean.Expr × Lean.Expr × Array Lean.Name × Bool × Option Lean.Term)) (declName? : Option Lean.Name) (instanceMaxHeartbeats : Nat) : Lean.MetaM Lean.Expr

Same as duper instance 2 except preprocessing is set to monomorphization only. Has the following options:

• preprocessing = monomorphization
• inhabitationReasoning = true
• selFunction = 4 (which corresponds to Zipperposition's default selection function)
• includeExpensiveRules = false

Equations

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

def Duper.runDuperInstance19 (formulas extraFormulas : List (Lean.Expr × Lean.Expr × Array Lean.Name × Bool × Option Lean.Term)) (declName? : Option Lean.Name) (instanceMaxHeartbeats : Nat) : Lean.MetaM Lean.Expr

Same as duper instance 3 except preprocessing is set to monomorphization only. Has the following options:

• preprocessing = monomorphization
• inhabitationReasoning = false
• selFunction = 11 (which corresponds to E's SelectMaxLComplexAvoidPosPred and Zipperposition's e_sel)
• includeExpensiveRules = true

Equations

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

def Duper.runDuperInstance20 (formulas extraFormulas : List (Lean.Expr × Lean.Expr × Array Lean.Name × Bool × Option Lean.Term)) (declName? : Option Lean.Name) (instanceMaxHeartbeats : Nat) : Lean.MetaM Lean.Expr

Same as duper instance 4 except preprocessing is set to monomorphization only. Has the following options:

• preprocessing = monomorphization
• inhabitationReasoning = true
• selFunction = 11 (which corresponds to E's SelectMaxLComplexAvoidPosPred and Zipperposition's e_sel)
• includeExpensiveRules = true

Equations

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

def Duper.runDuperInstance21 (formulas extraFormulas : List (Lean.Expr × Lean.Expr × Array Lean.Name × Bool × Option Lean.Term)) (declName? : Option Lean.Name) (instanceMaxHeartbeats : Nat) : Lean.MetaM Lean.Expr

Same as duper instance 5 except preprocessing is set to monomorphization only. Has the following options:

• preprocessing = no_preprocessing
• inhabitationReasoning = false
• selFunction = 13 (which corresponds to E's SelectComplexG and Zipperposition's e_sel3)
• includeExpensiveRules = false

Equations

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

def Duper.runDuperInstance22 (formulas extraFormulas : List (Lean.Expr × Lean.Expr × Array Lean.Name × Bool × Option Lean.Term)) (declName? : Option Lean.Name) (instanceMaxHeartbeats : Nat) : Lean.MetaM Lean.Expr

Same as duper instance 6 except preprocessing is set to monomorphization only. Has the following options:

• preprocessing = monomorphization
• inhabitationReasoning = true
• selFunction = 13 (which corresponds to E's SelectComplexG and Zipperposition's e_sel3)
• includeExpensiveRules = false

Equations

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

def Duper.runDuperInstance23 (formulas extraFormulas : List (Lean.Expr × Lean.Expr × Array Lean.Name × Bool × Option Lean.Term)) (declName? : Option Lean.Name) (instanceMaxHeartbeats : Nat) : Lean.MetaM Lean.Expr

Same as duper instance 7 except preprocessing is set to monomorphization only. Has the following options:

• preprocessing = monomorphization
• inhabitationReasoning = true
• selFunction = 2 (NoSelection)
• includeExpensiveRules = true

Equations

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

def Duper.runDuperInstance24 (formulas extraFormulas : List (Lean.Expr × Lean.Expr × Array Lean.Name × Bool × Option Lean.Term)) (declName? : Option Lean.Name) (instanceMaxHeartbeats : Nat) : Lean.MetaM Lean.Expr

Same as duper instance 8 except preprocessing is set to monomorphization only. Has the following options:

• preprocessing = monomorphization
• inhabitationReasoning = false
• selFunction = 2 (NoSelection)
• includeExpensiveRules = true

Equations

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

def Duper.runDuperInstance25 (formulas extraFormulas : List (Lean.Expr × Lean.Expr × Array Lean.Name × Bool × Option Lean.Term)) (declName? : Option Lean.Name) (instanceMaxHeartbeats : Nat) : Lean.MetaM Lean.Expr

Same as duper instance 1 except includeExpensiveRules is set to true. Has the following options:

• preprocessing = full
• inhabitationReasoning = false
• selFunction = 4 (which corresponds to Zipperposition's default selection function)
• includeExpensiveRules = true

Equations

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

def Duper.runDuperInstance26 (formulas extraFormulas : List (Lean.Expr × Lean.Expr × Array Lean.Name × Bool × Option Lean.Term)) (declName? : Option Lean.Name) (instanceMaxHeartbeats : Nat) : Lean.MetaM Lean.Expr

Same as duper instance 2 except includeExpensiveRules is set to true. Has the following options:

• preprocessing = full
• inhabitationReasoning = true
• selFunction = 4 (which corresponds to Zipperposition's default selection function)
• includeExpensiveRules = true

Equations

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

def Duper.runDuperInstance27 (formulas extraFormulas : List (Lean.Expr × Lean.Expr × Array Lean.Name × Bool × Option Lean.Term)) (declName? : Option Lean.Name) (instanceMaxHeartbeats : Nat) : Lean.MetaM Lean.Expr

Same as duper instance 3 except includeExpensiveRules is set to false. Has the following options:

• preprocessing = full
• inhabitationReasoning = false
• selFunction = 11 (which corresponds to E's SelectMaxLComplexAvoidPosPred and Zipperposition's e_sel)
• includeExpensiveRules = false

Equations

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

def Duper.runDuperInstance28 (formulas extraFormulas : List (Lean.Expr × Lean.Expr × Array Lean.Name × Bool × Option Lean.Term)) (declName? : Option Lean.Name) (instanceMaxHeartbeats : Nat) : Lean.MetaM Lean.Expr

Same as duper instance 4 except includeExpensiveRules is set to false. Has the following options:

• preprocessing = full
• inhabitationReasoning = true
• selFunction = 11 (which corresponds to E's SelectMaxLComplexAvoidPosPred and Zipperposition's e_sel)
• includeExpensiveRules = false

Equations

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

def Duper.runDuperInstance29 (formulas extraFormulas : List (Lean.Expr × Lean.Expr × Array Lean.Name × Bool × Option Lean.Term)) (declName? : Option Lean.Name) (instanceMaxHeartbeats : Nat) : Lean.MetaM Lean.Expr

Same as duper instance 5 except includeExpensiveRules is set to true. Has the following options:

• preprocessing = full
• inhabitationReasoning = false
• selFunction = 13 (which corresponds to E's SelectComplexG and Zipperposition's e_sel3)
• includeExpensiveRules = true

Equations

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

def Duper.runDuperInstance30 (formulas extraFormulas : List (Lean.Expr × Lean.Expr × Array Lean.Name × Bool × Option Lean.Term)) (declName? : Option Lean.Name) (instanceMaxHeartbeats : Nat) : Lean.MetaM Lean.Expr

Same as duper instance 6 except includeExpensiveRules is set to true. Has the following options:

• preprocessing = full
• inhabitationReasoning = true
• selFunction = 13 (which corresponds to E's SelectComplexG and Zipperposition's e_sel3)
• includeExpensiveRules = true

Equations

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

def Duper.runDuperInstance31 (formulas extraFormulas : List (Lean.Expr × Lean.Expr × Array Lean.Name × Bool × Option Lean.Term)) (declName? : Option Lean.Name) (instanceMaxHeartbeats : Nat) : Lean.MetaM Lean.Expr

Same as duper instance 7 except includeExpensiveRules is set to false. Has the following options:

• preprocessing = no_preprocessing
• inhabitationReasoning = true
• selFunction = 2 (NoSelection)
• includeExpensiveRules = false

Equations

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

def Duper.runDuperInstance32 (formulas extraFormulas : List (Lean.Expr × Lean.Expr × Array Lean.Name × Bool × Option Lean.Term)) (declName? : Option Lean.Name) (instanceMaxHeartbeats : Nat) : Lean.MetaM Lean.Expr

Same as duper instance 8 except includeExpensiveRules is set to false. Has the following options:

• preprocessing = no_preprocessing
• inhabitationReasoning = false
• selFunction = 2 (NoSelection)
• includeExpensiveRules = false

Equations

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

def Duper.runDuperInstance33 (formulas extraFormulas : List (Lean.Expr × Lean.Expr × Array Lean.Name × Bool × Option Lean.Term)) (declName? : Option Lean.Name) (instanceMaxHeartbeats : Nat) : Lean.MetaM Lean.Expr

Same as duper instance 9 except includeExpensiveRules is set to true. Has the following options:

• preprocessing = no_preprocessing
• inhabitationReasoning = false
• selFunction = 4 (which corresponds to Zipperposition's default selection function)
• includeExpensiveRules = true

Equations

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

def Duper.runDuperInstance34 (formulas extraFormulas : List (Lean.Expr × Lean.Expr × Array Lean.Name × Bool × Option Lean.Term)) (declName? : Option Lean.Name) (instanceMaxHeartbeats : Nat) : Lean.MetaM Lean.Expr

Same as duper instance 10 except includeExpensiveRules is set to true. Has the following options:

• preprocessing = no_preprocessing
• inhabitationReasoning = true
• selFunction = 4 (which corresponds to Zipperposition's default selection function)
• includeExpensiveRules = true

Equations

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

def Duper.runDuperInstance35 (formulas extraFormulas : List (Lean.Expr × Lean.Expr × Array Lean.Name × Bool × Option Lean.Term)) (declName? : Option Lean.Name) (instanceMaxHeartbeats : Nat) : Lean.MetaM Lean.Expr

Same as duper instance 11 except includeExpensiveRules is set to false. Has the following options:

• preprocessing = no_preprocessing
• inhabitationReasoning = false
• selFunction = 11 (which corresponds to E's SelectMaxLComplexAvoidPosPred and Zipperposition's e_sel)
• includeExpensiveRules = false

Equations

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

def Duper.runDuperInstance36 (formulas extraFormulas : List (Lean.Expr × Lean.Expr × Array Lean.Name × Bool × Option Lean.Term)) (declName? : Option Lean.Name) (instanceMaxHeartbeats : Nat) : Lean.MetaM Lean.Expr

Same as duper instance 12 except includeExpensiveRules is set to false. Has the following options:

• preprocessing = no_preprocessing
• inhabitationReasoning = true
• selFunction = 11 (which corresponds to E's SelectMaxLComplexAvoidPosPred and Zipperposition's e_sel)
• includeExpensiveRules = false

Equations

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

def Duper.runDuperInstance37 (formulas extraFormulas : List (Lean.Expr × Lean.Expr × Array Lean.Name × Bool × Option Lean.Term)) (declName? : Option Lean.Name) (instanceMaxHeartbeats : Nat) : Lean.MetaM Lean.Expr

Same as duper instance 13 except includeExpensiveRules is set to true. Has the following options:

• preprocessing = no_preprocessing
• inhabitationReasoning = false
• selFunction = 13 (which corresponds to E's SelectComplexG and Zipperposition's e_sel3)
• includeExpensiveRules = true

Equations

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

def Duper.runDuperInstance38 (formulas extraFormulas : List (Lean.Expr × Lean.Expr × Array Lean.Name × Bool × Option Lean.Term)) (declName? : Option Lean.Name) (instanceMaxHeartbeats : Nat) : Lean.MetaM Lean.Expr

Same as duper instance 14 except includeExpensiveRules is set to true. Has the following options:

• preprocessing = no_preprocessing
• inhabitationReasoning = true
• selFunction = 13 (which corresponds to E's SelectComplexG and Zipperposition's e_sel3)
• includeExpensiveRules = true

Equations

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

def Duper.runDuperInstance39 (formulas extraFormulas : List (Lean.Expr × Lean.Expr × Array Lean.Name × Bool × Option Lean.Term)) (declName? : Option Lean.Name) (instanceMaxHeartbeats : Nat) : Lean.MetaM Lean.Expr

Same as duper instance 15 except includeExpensiveRules is set to false. Has the following options:

• preprocessing = full
• inhabitationReasoning = true
• selFunction = 2 (NoSelection)
• includeExpensiveRules = false

Equations

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

def Duper.runDuperInstance40 (formulas extraFormulas : List (Lean.Expr × Lean.Expr × Array Lean.Name × Bool × Option Lean.Term)) (declName? : Option Lean.Name) (instanceMaxHeartbeats : Nat) : Lean.MetaM Lean.Expr

Same as duper instance 16 except includeExpensiveRules is set to false. Has the following options:

• preprocessing = full
• inhabitationReasoning = false
• selFunction = 2 (NoSelection)
• includeExpensiveRules = false

Equations

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

def Duper.runDuperInstance41 (formulas extraFormulas : List (Lean.Expr × Lean.Expr × Array Lean.Name × Bool × Option Lean.Term)) (declName? : Option Lean.Name) (instanceMaxHeartbeats : Nat) : Lean.MetaM Lean.Expr

Same as duper instance 17 except includeExpensiveRules is set to true. Has the following options:

• preprocessing = monomorphization
• inhabitationReasoning = false
• selFunction = 4 (which corresponds to Zipperposition's default selection function)
• includeExpensiveRules = true

Equations

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

def Duper.runDuperInstance42 (formulas extraFormulas : List (Lean.Expr × Lean.Expr × Array Lean.Name × Bool × Option Lean.Term)) (declName? : Option Lean.Name) (instanceMaxHeartbeats : Nat) : Lean.MetaM Lean.Expr

Same as duper instance 18 except includeExpensiveRules is set to true. Has the following options:

• preprocessing = monomorphization
• inhabitationReasoning = true
• selFunction = 4 (which corresponds to Zipperposition's default selection function)
• includeExpensiveRules = true

Equations

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

def Duper.runDuperInstance43 (formulas extraFormulas : List (Lean.Expr × Lean.Expr × Array Lean.Name × Bool × Option Lean.Term)) (declName? : Option Lean.Name) (instanceMaxHeartbeats : Nat) : Lean.MetaM Lean.Expr

Same as duper instance 19 except includeExpensiveRules is set to false. Has the following options:

• preprocessing = monomorphization
• inhabitationReasoning = false
• selFunction = 11 (which corresponds to E's SelectMaxLComplexAvoidPosPred and Zipperposition's e_sel)
• includeExpensiveRules = false

Equations

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

def Duper.runDuperInstance44 (formulas extraFormulas : List (Lean.Expr × Lean.Expr × Array Lean.Name × Bool × Option Lean.Term)) (declName? : Option Lean.Name) (instanceMaxHeartbeats : Nat) : Lean.MetaM Lean.Expr

Same as duper instance 20 except includeExpensiveRules is set to false. Has the following options:

• preprocessing = monomorphization
• inhabitationReasoning = true
• selFunction = 11 (which corresponds to E's SelectMaxLComplexAvoidPosPred and Zipperposition's e_sel)
• includeExpensiveRules = false

Equations

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

def Duper.runDuperInstance45 (formulas extraFormulas : List (Lean.Expr × Lean.Expr × Array Lean.Name × Bool × Option Lean.Term)) (declName? : Option Lean.Name) (instanceMaxHeartbeats : Nat) : Lean.MetaM Lean.Expr

Same as duper instance 21 except includeExpensiveRules is set to true. Has the following options:

• preprocessing = no_preprocessing
• inhabitationReasoning = false
• selFunction = 13 (which corresponds to E's SelectComplexG and Zipperposition's e_sel3)
• includeExpensiveRules = true

Equations

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

def Duper.runDuperInstance46 (formulas extraFormulas : List (Lean.Expr × Lean.Expr × Array Lean.Name × Bool × Option Lean.Term)) (declName? : Option Lean.Name) (instanceMaxHeartbeats : Nat) : Lean.MetaM Lean.Expr

Same as duper instance 22 except includeExpensiveRules is set to true. Has the following options:

• preprocessing = monomorphization
• inhabitationReasoning = true
• selFunction = 13 (which corresponds to E's SelectComplexG and Zipperposition's e_sel3)
• includeExpensiveRules = true

Equations

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

def Duper.runDuperInstance47 (formulas extraFormulas : List (Lean.Expr × Lean.Expr × Array Lean.Name × Bool × Option Lean.Term)) (declName? : Option Lean.Name) (instanceMaxHeartbeats : Nat) : Lean.MetaM Lean.Expr

Same as duper instance 23 except includeExpensiveRules is set to false. Has the following options:

• preprocessing = monomorphization
• inhabitationReasoning = true
• selFunction = 2 (NoSelection)
• includeExpensiveRules = false

Equations

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

def Duper.runDuperInstance48 (formulas extraFormulas : List (Lean.Expr × Lean.Expr × Array Lean.Name × Bool × Option Lean.Term)) (declName? : Option Lean.Name) (instanceMaxHeartbeats : Nat) : Lean.MetaM Lean.Expr

Same as duper instance 24 except includeExpensiveRules is set to false. Has the following options:

• preprocessing = monomorphization
• inhabitationReasoning = false
• selFunction = 2 (NoSelection)
• includeExpensiveRules = false

Equations

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

def Duper.instanceHasInhabitationReasoning {m : Type → Type} [Monad m] [Lean.MonadError m] (n : Nat) : m Bool

Returns true iff the given duper instance n has inhabitation reasoning enabled. Returns false iff the given duper instance n has inhabitation reasoning disabled. Throws an error if given an invalid duper instance.

def Duper.getInstanceWithInhabitationReasoning (n : Nat) : Option (Nat × (List (Lean.Expr × Lean.Expr × Array Lean.Name × Bool × Option Lean.Term) → List (Lean.Expr × Lean.Expr × Array Lean.Name × Bool × Option Lean.Term) → Option Lean.Name → Nat → Lean.MetaM Lean.Expr))

If the given duper instance n has inhabitation reasoning disabled and there is another instance m that is identical except that it has inhabitation reasoning enabled, then getInstanceWithInhabitationReasoning returns some m. Otherwise, getInstanceWithInhabitationReasoning returns none.

Equations

• Duper.getInstanceWithInhabitationReasoning 1 = some (2, Duper.runDuperInstance2)
• Duper.getInstanceWithInhabitationReasoning 3 = some (4, Duper.runDuperInstance4)
• Duper.getInstanceWithInhabitationReasoning 5 = some (6, Duper.runDuperInstance6)
• Duper.getInstanceWithInhabitationReasoning 8 = some (7, Duper.runDuperInstance7)
• Duper.getInstanceWithInhabitationReasoning 9 = some (10, Duper.runDuperInstance10)
• Duper.getInstanceWithInhabitationReasoning 11 = some (12, Duper.runDuperInstance12)
• Duper.getInstanceWithInhabitationReasoning 13 = some (14, Duper.runDuperInstance14)
• Duper.getInstanceWithInhabitationReasoning 16 = some (15, Duper.runDuperInstance15)
• Duper.getInstanceWithInhabitationReasoning 17 = some (18, Duper.runDuperInstance18)
• Duper.getInstanceWithInhabitationReasoning 19 = some (20, Duper.runDuperInstance20)
• Duper.getInstanceWithInhabitationReasoning 21 = some (22, Duper.runDuperInstance22)
• Duper.getInstanceWithInhabitationReasoning 24 = some (23, Duper.runDuperInstance23)
• Duper.getInstanceWithInhabitationReasoning 25 = some (26, Duper.runDuperInstance26)
• Duper.getInstanceWithInhabitationReasoning 27 = some (28, Duper.runDuperInstance28)
• Duper.getInstanceWithInhabitationReasoning 29 = some (30, Duper.runDuperInstance30)
• Duper.getInstanceWithInhabitationReasoning 32 = some (31, Duper.runDuperInstance31)
• Duper.getInstanceWithInhabitationReasoning 33 = some (34, Duper.runDuperInstance34)
• Duper.getInstanceWithInhabitationReasoning 35 = some (36, Duper.runDuperInstance36)
• Duper.getInstanceWithInhabitationReasoning 37 = some (38, Duper.runDuperInstance38)
• Duper.getInstanceWithInhabitationReasoning 40 = some (39, Duper.runDuperInstance39)
• Duper.getInstanceWithInhabitationReasoning 41 = some (42, Duper.runDuperInstance42)
• Duper.getInstanceWithInhabitationReasoning 43 = some (44, Duper.runDuperInstance44)
• Duper.getInstanceWithInhabitationReasoning 45 = some (46, Duper.runDuperInstance46)
• Duper.getInstanceWithInhabitationReasoning 48 = some (47, Duper.runDuperInstance47)
• Duper.getInstanceWithInhabitationReasoning n = none

def Duper.getInstanceWithoutInhabitationReasoning (n : Nat) : Option (Nat × (List (Lean.Expr × Lean.Expr × Array Lean.Name × Bool × Option Lean.Term) → List (Lean.Expr × Lean.Expr × Array Lean.Name × Bool × Option Lean.Term) → Option Lean.Name → Nat → Lean.MetaM Lean.Expr))

If the given duper instance n has inhabitation reasoning enabled and there is another instance m that is identical except that it has inhabitation reasoning disabled, then getInstanceWithoutInhabitationReasoning returns some m. Otherwise, getInstanceWithoutInhabitationReasoning returns none.

Equations

• Duper.getInstanceWithoutInhabitationReasoning 2 = some (1, Duper.runDuperInstance1)
• Duper.getInstanceWithoutInhabitationReasoning 4 = some (3, Duper.runDuperInstance3)
• Duper.getInstanceWithoutInhabitationReasoning 6 = some (5, Duper.runDuperInstance5)
• Duper.getInstanceWithoutInhabitationReasoning 7 = some (8, Duper.runDuperInstance8)
• Duper.getInstanceWithoutInhabitationReasoning 10 = some (9, Duper.runDuperInstance9)
• Duper.getInstanceWithoutInhabitationReasoning 12 = some (11, Duper.runDuperInstance11)
• Duper.getInstanceWithoutInhabitationReasoning 14 = some (13, Duper.runDuperInstance13)
• Duper.getInstanceWithoutInhabitationReasoning 15 = some (16, Duper.runDuperInstance16)
• Duper.getInstanceWithoutInhabitationReasoning 18 = some (17, Duper.runDuperInstance17)
• Duper.getInstanceWithoutInhabitationReasoning 20 = some (19, Duper.runDuperInstance19)
• Duper.getInstanceWithoutInhabitationReasoning 22 = some (21, Duper.runDuperInstance21)
• Duper.getInstanceWithoutInhabitationReasoning 23 = some (24, Duper.runDuperInstance24)
• Duper.getInstanceWithoutInhabitationReasoning 26 = some (25, Duper.runDuperInstance25)
• Duper.getInstanceWithoutInhabitationReasoning 28 = some (27, Duper.runDuperInstance27)
• Duper.getInstanceWithoutInhabitationReasoning 30 = some (29, Duper.runDuperInstance29)
• Duper.getInstanceWithoutInhabitationReasoning 31 = some (32, Duper.runDuperInstance32)
• Duper.getInstanceWithoutInhabitationReasoning 34 = some (33, Duper.runDuperInstance33)
• Duper.getInstanceWithoutInhabitationReasoning 36 = some (35, Duper.runDuperInstance35)
• Duper.getInstanceWithoutInhabitationReasoning 38 = some (37, Duper.runDuperInstance37)
• Duper.getInstanceWithoutInhabitationReasoning 39 = some (40, Duper.runDuperInstance40)
• Duper.getInstanceWithoutInhabitationReasoning 42 = some (41, Duper.runDuperInstance41)
• Duper.getInstanceWithoutInhabitationReasoning 44 = some (43, Duper.runDuperInstance43)
• Duper.getInstanceWithoutInhabitationReasoning 46 = some (45, Duper.runDuperInstance45)
• Duper.getInstanceWithoutInhabitationReasoning 47 = some (48, Duper.runDuperInstance48)
• Duper.getInstanceWithoutInhabitationReasoning n = none

def Duper.getInstanceWithExpensiveRules (n : Nat) : Option (Nat × (List (Lean.Expr × Lean.Expr × Array Lean.Name × Bool × Option Lean.Term) → List (Lean.Expr × Lean.Expr × Array Lean.Name × Bool × Option Lean.Term) → Option Lean.Name → Nat → Lean.MetaM Lean.Expr))

If the given duper instance n has includeExpensiveRules set to false and there is another instance m that is identical except that it has includeExpensiveRules set to true, then getInstanceWithExpensiveRules returns some m. Otherwise, getInstanceWithExpensiveRules returns none.

Equations

• Duper.getInstanceWithExpensiveRules 1 = some (25, Duper.runDuperInstance25)
• Duper.getInstanceWithExpensiveRules 2 = some (26, Duper.runDuperInstance26)
• Duper.getInstanceWithExpensiveRules 5 = some (29, Duper.runDuperInstance29)
• Duper.getInstanceWithExpensiveRules 6 = some (30, Duper.runDuperInstance30)
• Duper.getInstanceWithExpensiveRules 9 = some (33, Duper.runDuperInstance33)
• Duper.getInstanceWithExpensiveRules 10 = some (34, Duper.runDuperInstance34)
• Duper.getInstanceWithExpensiveRules 13 = some (37, Duper.runDuperInstance37)
• Duper.getInstanceWithExpensiveRules 14 = some (38, Duper.runDuperInstance38)
• Duper.getInstanceWithExpensiveRules 17 = some (41, Duper.runDuperInstance41)
• Duper.getInstanceWithExpensiveRules 18 = some (42, Duper.runDuperInstance42)
• Duper.getInstanceWithExpensiveRules 21 = some (45, Duper.runDuperInstance45)
• Duper.getInstanceWithExpensiveRules 22 = some (46, Duper.runDuperInstance46)
• Duper.getInstanceWithExpensiveRules 27 = some (3, Duper.runDuperInstance3)
• Duper.getInstanceWithExpensiveRules 28 = some (4, Duper.runDuperInstance4)
• Duper.getInstanceWithExpensiveRules 31 = some (7, Duper.runDuperInstance7)
• Duper.getInstanceWithExpensiveRules 32 = some (8, Duper.runDuperInstance8)
• Duper.getInstanceWithExpensiveRules 35 = some (11, Duper.runDuperInstance11)
• Duper.getInstanceWithExpensiveRules 36 = some (12, Duper.runDuperInstance12)
• Duper.getInstanceWithExpensiveRules 39 = some (15, Duper.runDuperInstance15)
• Duper.getInstanceWithExpensiveRules 40 = some (16, Duper.runDuperInstance16)
• Duper.getInstanceWithExpensiveRules 43 = some (19, Duper.runDuperInstance19)
• Duper.getInstanceWithExpensiveRules 44 = some (20, Duper.runDuperInstance20)
• Duper.getInstanceWithExpensiveRules 47 = some (23, Duper.runDuperInstance23)
• Duper.getInstanceWithExpensiveRules 48 = some (24, Duper.runDuperInstance24)
• Duper.getInstanceWithExpensiveRules n = none

def Duper.getInstanceWithoutExpensiveRules (n : Nat) : Option (Nat × (List (Lean.Expr × Lean.Expr × Array Lean.Name × Bool × Option Lean.Term) → List (Lean.Expr × Lean.Expr × Array Lean.Name × Bool × Option Lean.Term) → Option Lean.Name → Nat → Lean.MetaM Lean.Expr))

If the given duper instance n has includeExpensiveRules set to true and there is another instance m that is identical except that it has includeExpensiveRules set to false, then getInstanceWithoutExpensiveRules returns some m. Otherwise, getInstanceWithoutExpensiveRules returns none.

Equations

• Duper.getInstanceWithoutExpensiveRules 25 = some (1, Duper.runDuperInstance1)
• Duper.getInstanceWithoutExpensiveRules 26 = some (2, Duper.runDuperInstance2)
• Duper.getInstanceWithoutExpensiveRules 29 = some (5, Duper.runDuperInstance5)
• Duper.getInstanceWithoutExpensiveRules 30 = some (6, Duper.runDuperInstance6)
• Duper.getInstanceWithoutExpensiveRules 33 = some (9, Duper.runDuperInstance9)
• Duper.getInstanceWithoutExpensiveRules 34 = some (10, Duper.runDuperInstance10)
• Duper.getInstanceWithoutExpensiveRules 37 = some (13, Duper.runDuperInstance13)
• Duper.getInstanceWithoutExpensiveRules 38 = some (14, Duper.runDuperInstance14)
• Duper.getInstanceWithoutExpensiveRules 41 = some (17, Duper.runDuperInstance17)
• Duper.getInstanceWithoutExpensiveRules 42 = some (18, Duper.runDuperInstance18)
• Duper.getInstanceWithoutExpensiveRules 45 = some (21, Duper.runDuperInstance21)
• Duper.getInstanceWithoutExpensiveRules 46 = some (22, Duper.runDuperInstance22)
• Duper.getInstanceWithoutExpensiveRules 3 = some (27, Duper.runDuperInstance27)
• Duper.getInstanceWithoutExpensiveRules 4 = some (28, Duper.runDuperInstance28)
• Duper.getInstanceWithoutExpensiveRules 7 = some (31, Duper.runDuperInstance31)
• Duper.getInstanceWithoutExpensiveRules 8 = some (32, Duper.runDuperInstance32)
• Duper.getInstanceWithoutExpensiveRules 11 = some (35, Duper.runDuperInstance35)
• Duper.getInstanceWithoutExpensiveRules 12 = some (36, Duper.runDuperInstance36)
• Duper.getInstanceWithoutExpensiveRules 15 = some (39, Duper.runDuperInstance39)
• Duper.getInstanceWithoutExpensiveRules 16 = some (40, Duper.runDuperInstance40)
• Duper.getInstanceWithoutExpensiveRules 19 = some (43, Duper.runDuperInstance43)
• Duper.getInstanceWithoutExpensiveRules 20 = some (44, Duper.runDuperInstance44)
• Duper.getInstanceWithoutExpensiveRules 23 = some (47, Duper.runDuperInstance47)
• Duper.getInstanceWithoutExpensiveRules 24 = some (48, Duper.runDuperInstance48)
• Duper.getInstanceWithoutExpensiveRules n = none

def Duper.runDuperPortfolioMode (formulas extraFormulas : List (Lean.Expr × Lean.Expr × Array Lean.Name × Bool × Option Lean.Term)) (declName? : Option Lean.Name) (configOptions : ConfigurationOptions) (duperStxInfo : Option (Lean.Syntax × Lean.Syntax × Lean.Syntax.TSepArray `term "," × Option (Lean.Syntax.TSepArray `term ",") × Bool)) : Lean.MetaM Lean.Expr

Implements duper calls when portfolio mode is enabled. If duperStxInfo is not none and runDuperPortfolioMode succeeds in deriving a contradiction, then Std.Tactic.TryThis.addSuggestion will be used to give the user a more specific invocation of duper that can reproduce the proof (without having to run duper in portfolio mode). As with the other runDuper functions, runDuperPortfolioMode ultimately returns a proof if successful and throws an error if unsuccessful.

Equations

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