VCGen Naming Helpers

Utilities for choosing user-facing binder and support-hypothesis names in VCGen tactics.

def OracleComp.ProgramLogic.isUsableBinderName (name : Lean.Name) : Bool

def OracleComp.ProgramLogic.mkSupportHypName (name : Lean.Name) : Lean.Name

def OracleComp.ProgramLogic.freshUserNameLike (base : Lean.Name) : Lean.Elab.Tactic.TacticM Lean.Name

def OracleComp.ProgramLogic.freshenSuggestedNames (names : Array Lean.Name) : Lean.Elab.Tactic.TacticM (Array Lean.Name)

def OracleComp.ProgramLogic.binderNameFromExpr? (e : Lean.Expr) : Option Lean.Name

def OracleComp.ProgramLogic.getBindLambdaName? (comp : Lean.Expr) : Option Lean.Name

def OracleComp.ProgramLogic.probGoalComp? (target : Lean.Expr) : Option Lean.Expr

def OracleComp.ProgramLogic.getLeadingBinderNames (target : Lean.Expr) : Array Lean.Name

partial def OracleComp.ProgramLogic.getLeadingBinderNames.go (e : Lean.Expr) (acc : Array Lean.Name) : Array Lean.Name

def OracleComp.ProgramLogic.getGoalBindVarName? : Lean.Elab.Tactic.TacticM (Option Lean.Name)

def OracleComp.ProgramLogic.getSuggestedIntroNames (count : ℕ) : Lean.Elab.Tactic.TacticM (Array Lean.Name)

def OracleComp.ProgramLogic.getProbCongrNames (supportSensitive : Bool) : Lean.Elab.Tactic.TacticM (Array Lean.Name)

def OracleComp.ProgramLogic.getRelBindNames : Lean.Elab.Tactic.TacticM (Array Lean.Name)

def OracleComp.ProgramLogic.introMainGoalNames (names : Array Lean.Name) : Lean.Elab.Tactic.TacticM Bool

def OracleComp.ProgramLogic.introAllGoalsNames (names : Array Lean.Name) : Lean.Elab.Tactic.TacticM Unit

def OracleComp.ProgramLogic.renameInaccessibleNames (names : Array Lean.Name) : Lean.Elab.Tactic.TacticM Unit

def OracleComp.ProgramLogic.renderAsClause (names : Array Lean.Name) : String