TacticUtil

This module provides small utilities shared by the MRiscX tactics.

def findHypTypeM? (ctx : Lean.LocalContext) (n : Lean.Name) : Lean.MetaM (Option Lean.Expr)

Find the type of the local hypothesis named n in ctx, if present.

Equations

• findHypTypeM? ctx n = ctx.findDeclM? fun (decl : Lean.LocalDecl) => if (decl.userName == n) = true then pure (some decl.type) else pure none

def findHypTypeM (ctx : Lean.LocalContext) (n : Lean.Name) : Lean.MetaM Lean.Expr

Find the type of the local hypothesis named n in ctx, throwing if absent.

Equations

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