Documentation

Lean.Elab.Tactic.Conv.Congr

def Lean.Elab.Tactic.Conv.isImplies (e : Lean.Expr) :

Lean.MetaM Bool

Equations

Lean.Elab.Tactic.Conv.isImplies e = if Lean.Expr.isArrow e = true then Lean.Meta.isProp (Lean.Expr.bindingDomain! e) <&&> Lean.Meta.isProp (Lean.Expr.bindingBody! e) else pure false

def Lean.Elab.Tactic.Conv.congr (mvarId : Lean.MVarId) :

Lean.MetaM (List Lean.MVarId)

Equations

Lean.Elab.Tactic.Conv.congr mvarId = Lean.Meta.withMVarContext mvarId do let discr ← Lean.Elab.Tactic.Conv.getLhsRhsCore mvarId let x : Lean.Expr × Lean.Expr := discr match x with | (lhs, rhs) => do let lhs ← Lean.Meta.instantiateMVars lhs let cls : Lean.Name := `Meta.debug let a ← Lean.isTracingEnabledFor cls let _do_jp : Unit → Lean.MetaM (List Lean.MVarId) := fun y => do let a ← Lean.Elab.Tactic.Conv.isImplies lhs if a = true then Lean.Elab.Tactic.Conv.congrImplies mvarId else if Lean.Expr.isApp lhs = true then Lean.Elab.Tactic.Conv.congrApp mvarId lhs rhs else Lean.throwError (Lean.toMessageData "invalid 'congr' conv tactic, application or implication expected" ++ Lean.toMessageData (Lean.indentExpr lhs) ++ Lean.toMessageData "") if a = true then do let y ← Lean.addTrace cls (Lean.toMessageData "" ++ Lean.toMessageData lhs ++ Lean.toMessageData " = " ++ Lean.toMessageData rhs ++ Lean.toMessageData "") _do_jp y else do let y ← pure PUnit.unit _do_jp y

def Lean.Elab.Tactic.Conv.evalCongr :

Lean.Elab.Tactic.Tactic

Equations

Lean.Elab.Tactic.Conv.evalCongr stx = do let a ← Lean.Elab.Tactic.getMainGoal let a ← liftM (Lean.Elab.Tactic.Conv.congr a) Lean.Elab.Tactic.replaceMainGoal a

def Lean.Elab.Tactic.Conv.evalLhs :

Lean.Elab.Tactic.Tactic

Equations

Lean.Elab.Tactic.Conv.evalLhs stx = do let a ← Lean.Elab.Tactic.getMainGoal let mvarIds ← liftM (Lean.Elab.Tactic.Conv.congr a) Lean.Elab.Tactic.Conv.selectIdx "lhs" mvarIds (Int.ofNat (List.length mvarIds) - 2)

def Lean.Elab.Tactic.Conv.evalRhs :

Lean.Elab.Tactic.Tactic

Equations

Lean.Elab.Tactic.Conv.evalRhs stx = do let a ← Lean.Elab.Tactic.getMainGoal let mvarIds ← liftM (Lean.Elab.Tactic.Conv.congr a) Lean.Elab.Tactic.Conv.selectIdx "rhs" mvarIds (Int.ofNat (List.length mvarIds) - 1)

def Lean.Elab.Tactic.Conv.evalArg :

Lean.Elab.Tactic.Tactic

Equations

Lean.Elab.Tactic.Conv.evalArg stx = let discr := stx; if Lean.Syntax.isOfKind discr `Lean.Parser.Tactic.Conv.arg = true then let discr_1 := Lean.Syntax.getArg discr 0; let discr := Lean.Syntax.getArg discr 1; let i := discr; let i := Option.getD (Lean.Syntax.isNatLit? i) 0; let _do_jp := fun y => let i := i - 1; do let a ← Lean.Elab.Tactic.getMainGoal let mvarIds ← liftM (Lean.Elab.Tactic.Conv.congr a) Lean.Elab.Tactic.Conv.selectIdx "arg" mvarIds (Int.ofNat i); if (i == 0) = true then do let y ← Lean.throwError (Lean.toMessageData "invalid 'arg' conv tactic, index must be greater than 0") _do_jp y else do let y ← pure PUnit.unit _do_jp y else let discr := stx; Lean.Elab.throwUnsupportedSyntax

def Lean.Elab.Tactic.Conv.evalExt :

Lean.Elab.Tactic.Tactic

Equations

Lean.Elab.Tactic.Conv.evalExt stx = let ids := Lean.Syntax.getArgs (Lean.Syntax.getOp stx 1); if Array.isEmpty ids = true then Lean.Elab.Tactic.Conv.ext none else do let r ← forIn ids PUnit.unit fun id r => do Lean.withRef id (Lean.Elab.Tactic.Conv.ext (some (Lean.Syntax.getId id))) pure (ForInStep.yield PUnit.unit) let x : PUnit := r pure PUnit.unit