opaque Duper.duper.printTimeInformation : Lean.Option Bool

opaque Duper.duper.ignoreUnusableFacts : Lean.Option Bool

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

Equations

• Duper.getPrintTimeInformation opts = Lean.Option.get opts Duper.duper.printTimeInformation

def Duper.getPrintTimeInformationM : Lean.CoreM Bool

Equations

• Duper.getPrintTimeInformationM = do let opts ← Lean.getOptions pure (Duper.getPrintTimeInformation opts)

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

Equations

• Duper.getIgnoreUnusableFacts opts = Lean.Option.get opts Duper.duper.ignoreUnusableFacts

def Duper.getIgnoreUnusableFactsM : Lean.CoreM Bool

Equations

• Duper.getIgnoreUnusableFactsM = do let opts ← Lean.getOptions pure (Duper.getIgnoreUnusableFacts opts)

def Duper.addRecAsFact (recVal : Lean.RecursorVal) : Lean.Elab.Tactic.TacticM (List (Lean.Expr × Lean.Expr × Array Lean.Name))

Produces definional equations for a recursor recVal such as

@Nat.rec m z s (Nat.succ n) = s n (@Nat.rec m z s n)

The returned list contains one equation for each constructor, a proof of the equation, and the contained level parameters.

Equations

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

def Duper.elabFact (stx : Lean.Term) : Lean.Elab.Tactic.TacticM (Array (Lean.Expr × Lean.Expr × Array Lean.Name))

From a user-provided fact stx, produce a suitable fact, its proof, and a list of universe parameter names

Equations

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

def Duper.elabFact.elabFactAux (stx : Lean.Term) : Lean.Elab.Tactic.TacticM (Lean.Expr × Lean.Expr × Array Lean.Name)

Equations

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

def Duper.collectLCtxAssumptions (goalDecls : Array Lean.LocalDecl) : Lean.MetaM (List (Lean.Expr × Lean.Expr × Array Lean.Name × Bool × Option Lean.Term))

Helper function for collectAssumptions that collects all local decls in the local context that are propositions.

Equations

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

def Duper.collectAssumptions (facts : Array Lean.Term) (withAllLCtx : Bool) (goalDecls : Array Lean.LocalDecl) : Lean.Elab.Tactic.TacticM (List (Lean.Expr × Lean.Expr × Array Lean.Name × Bool × Option Lean.Term))

Formulas in Duper are represented as a tuple containing the following:

• The fact that Duper can use
• A proof that said fact is true (if the fact is p then second argument of the tuple is a proof of p = True)
• An array of universe level parameter names
• A boolean indicating whether the fact came from the original target
• If the fact is a user-provided non-lctx fact, then the Term that was used to indicate said fact

Equations

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

def Duper.removeDuperStar (facts : Lean.Syntax.TSepArray [`Duper.duperStar, `term] ",") : Bool × Lean.Syntax.TSepArray `term ","

Given a Syntax.TSepArray of facts provided by the user (which may include * to indicate that duper should read in the full local context) removeDuperStar returns the Syntax.TSepArray with * removed and a boolean that indicates whether * was included in the original input.

Equations

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

def Duper.parseConfigOptions (configOptionsStx : Lean.TSyntaxArray `Duper.configOption) : Lean.Elab.Tactic.TacticM ConfigurationOptions

Determines what configuration options Duper should use based on a (potentially partial) set of configuration options passed in by the user. If configuration options are not fully specified, this function gives the following default options:

• Enables portfolio mode by default unless a portfolio instance is specified
• Sets the portfolio instance to 0 by default if portfolio mode is explicitly disabled and no instance is specified
• Sets other options to none by default

Additionally, this function throws an error if the user attempts to explicitly enable portfolio mode and specify a portfolio instance, and it throws a warning if the user attempts to specify a portfolio instance (other than 0) and additional configuration options.

Equations

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

def Duper.getGoalDecls (lctxBeforeIntros lctxAfterIntros : Lean.LocalContext) : Array Lean.LocalDecl

When duper is called, the first thing the tactic does is call the tactic intros; apply Classical.byContradiction _; intro. Even when * is not included in the duper invocation (meaning the user does not want duper to collect all the facts in the local context), it is necessary to include the negated goal. This negated goal may take the form of arbitrarily many declarations in the local context if the duper is asked to solve a goal of the form p1 → p2 → p3 → ... pn. So to ensure that duper is able to see the whole original goal, getGoalDecls compares the local context before calling intros; apply Classical.byContradiction _; intro and after calling intros; apply Classical.byContradiction _; intro. The local declarations that are part of the latter lctx but not the former are considered goal decls and are to be returned so that Duper can know to collect them in collectAssumptions.

Equations

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

def Duper.evalDuper : Lean.Elab.Tactic.Tactic

Equations

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

def Duper.evalDuperTrace : Lean.Elab.Tactic.Tactic

Equations

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

def Duper.duper_no_timing : Lean.ParserDescr

Note: This tactic exists primarily for internal github testing and is not intended for external use.

Equations

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

def Duper.evalDuperNoTiming : Lean.Elab.Tactic.Tactic

Equations

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