How to get the type of the first argument to `cases'`

Stream: mathlib4

[Jeremy Tan]

The code defining cases' in mathlib is as follows.

elab (name := cases') "cases' " tgts:(Parser.Tactic.casesTarget,+) usingArg:((" using " ident)?)
  withArg:((" with" (ppSpace colGt binderIdent)+)?) : tactic => do
  let (targets, toTag) ← elabCasesTargets tgts.1.getSepArgs
  let g :: gs ← getUnsolvedGoals | throwNoGoalsToBeSolved
  g.withContext do
    let elimInfo ← getElimNameInfo usingArg targets (induction := false)
    let targets ← addImplicitTargets elimInfo targets
    let result ← withRef tgts <| ElimApp.mkElimApp elimInfo targets (← g.getTag)
    let elimArgs := result.elimApp.getAppArgs
    let targets ← elimInfo.targetsPos.mapM (instantiateMVars elimArgs[·]!)
    let motive := elimArgs[elimInfo.motivePos]!
    let g ← generalizeTargetsEq g (← inferType motive) targets
    let (targetsNew, g) ← g.introN targets.size
    g.withContext do
      ElimApp.setMotiveArg g motive.mvarId! targetsNew
      g.assign result.elimApp
      let subgoals ← ElimApp.evalNames elimInfo result.alts withArg
         (numEqs := targets.size) (toClear := targetsNew) (toTag := toTag)
      setGoals <| subgoals.toList ++ gs

How could I modify this code to print out (using logInfo) the type of the head of the first argument passed to cases'? For example with cases' eq_or_lt_of_le (hz i hi) with hz hz I want Or to be printed out, for cases' i with j with i a Nat I want Nat to be printed out, etc.

[Jeremy Tan]

And if it is a type with explicit constructors (i.e. cases' generates one case called intro) I want to be able to know that as well

[Damiano Testa]

Is docs#Lean.Meta.inferType what you are looking for?

[Jeremy Tan]

Damiano Testa said:

Is docs#Lean.Meta.inferType what you are looking for?

No:

application type mismatch
  inferType tgts.raw.getSepArgs
argument
  tgts.raw.getSepArgs
has type
  Array Syntax : Type
but is expected to have type
  Expr : Type

[Jeremy Tan]

Furthermore the output type of inferType, MetaM Expr, cannot be printed

[Yaël Dillies]

Why are you apply getSetArgs before applying inferType? Also surely Expr can be printed? and you get that when binding a MetaM Expr

[Jeremy Tan]

What is binding?

[Yaël Dillies]

If you have e : MetaM Expr, then doing let e' ← e inside a do block "binds" e' to e, in the sense that it's applying the monadic bind.

[Jeremy Tan]

This does compile, but I need to get the number of subgoals generated by each and every use of cases' first before seeing if it gets me the head of the type properly

let zzz ← inferType (targets.get! 0)
logInfoAt tgts m!"{zzz} {targets} {subgoals.toList.length}"

[Jeremy Tan]

(A Lean modification is running right now)

[Jeremy Tan]

All right @Yaël Dillies, but how do I disable pretty printing when logging zzz above?

[Jeremy Tan]

oh

[Jeremy Tan]

let zzz ← inferType (targets.get! 0)
      logInfoAt tgts m!"{zzz.setPPExplicit true} {targets} {subgoals.toList.length}"