def TLA.ProofMode.temporalHypLoc : Lean.ParserDescr

Syntax for referring to a proof-mode hypothesis by name or index.

Equations

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

inductive TLA.ProofMode.TemporalHypLoc : Type

Locations for proof-mode hypotheses. Can be a name or an index.

• byName (name : String) : TemporalHypLoc
• byIdx (idx : Nat) : TemporalHypLoc

def TLA.ProofMode.parseTemporalHypLoc (pos : Lean.Syntax) (errorMsg : Lean.MessageData) : Lean.Elab.Tactic.TacticM TemporalHypLoc

Parse a temporalHypLoc syntax into a TemporalHypLoc.

Equations

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

def TLA.ProofMode.quoteTemporalHypLoc : TemporalHypLoc → Lean.Elab.Tactic.TacticM (Lean.TSyntax `TLA.ProofMode.temporalHypLoc)

Quote a TemporalHypLoc back into temporalHypLoc syntax.

Equations

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

def TLA.ProofMode.quoteTemporalHypLocToTerm : TemporalHypLoc → Lean.TSyntax `term

Quote a TemporalHypLoc as a term.

Equations

• TLA.ProofMode.quoteTemporalHypLocToTerm (TLA.ProofMode.TemporalHypLoc.byName name) = Lean.quote `term name
• TLA.ProofMode.quoteTemporalHypLocToTerm (TLA.ProofMode.TemporalHypLoc.byIdx idx) = Lean.quote `term idx

def TLA.ProofMode.findByTemporalHypLocOpt {α : Type u_1} (xs : List (String × α)) : TemporalHypLoc → Option (String × α)

Look up a hypothesis by location, returning none if absent.

Equations

• TLA.ProofMode.findByTemporalHypLocOpt xs (TLA.ProofMode.TemporalHypLoc.byName name) = List.find? (fun (x : String × α) => x.fst == name) xs
• TLA.ProofMode.findByTemporalHypLocOpt xs (TLA.ProofMode.TemporalHypLoc.byIdx idx) = xs[idx]?

def TLA.ProofMode.findByTemporalHypLoc {m : Type → Type} {α : Type} [Monad m] [Lean.MonadError m] (xs : List (String × α)) (loc : TemporalHypLoc) (errorMsgPrefix errorMsgSuffix : String) : m (String × α)

Look up a hypothesis by location, throwing an error if absent.

Equations

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

def TLA.ProofMode.temporalHypNameOfBareTermOpt {α : Type u_1} (hyps : List (String × α)) (tm : Lean.Term) : Lean.Elab.Tactic.TacticM (Option String)

If tm is a bare identifier that names a proof-mode hypothesis in hyps, return that name. Lean locals shadow proof-mode hypotheses.

Equations

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

def TLA.ProofMode.temporalHypLocOfBareTermOpt {α : Type u_1} (hyps : List (String × α)) (tm : Lean.Term) : Lean.Elab.Tactic.TacticM (Option TemporalHypLoc)

Interpret a bare term as a hypothesis location, if it names one.

Equations

• TLA.ProofMode.temporalHypLocOfBareTermOpt hyps tm = do let __do_lift ← TLA.ProofMode.temporalHypNameOfBareTermOpt hyps tm pure (Option.map TLA.ProofMode.TemporalHypLoc.byName __do_lift)

structure TLA.ProofMode.RewriteLocation : Type

Locations for rewrite/simp-like tactics.

• idxs : Array Nat

  The hypothesis indices targeted by a rewrite location.

• includeGoal : Bool

  Whether the rewrite location includes the goal.

• isWildCard : Bool

  Whether the rewrite location is a wildcard.

def TLA.ProofMode.parseRewriteLocation (hyps : List (String × Lean.Expr)) (loc? : Option (Lean.TSyntax `Lean.Parser.Tactic.location)) (errorMsgPrefix : String) : Lean.Elab.Tactic.TacticM RewriteLocation

Parse a rewrite location into the targeted indices.

Equations

• One or more equations did not get rendered due to their size.
• TLA.ProofMode.parseRewriteLocation hyps none errorMsgPrefix = pure { idxs := #[], includeGoal := true, isWildCard := false }