Recursor and RecursorInfo

Stream: metaprogramming / tactics

[Leni Aniva]

Why is Lean.Syntax.rec_2 not recognized as a recursor by Meta.mkRecursorInfo? Its ConstantInfo is even registered as RecursorVal.

#check Lean.Syntax.rec_2
#eval do
  let name := `Lean.Syntax.rec_2
  let info ← Meta.mkRecursorInfo name

It's type is

Lean.Syntax.rec_2.{u} {motive_1 : Syntax → Sort u} {motive_2 : Array Syntax → Sort u} {motive_3 : List Syntax → Sort u}
  (missing : motive_1 Syntax.missing)
  (node :
    (info : SourceInfo) →
      (kind : SyntaxNodeKind) → (args : Array Syntax) → motive_2 args → motive_1 (Syntax.node info kind args))
  (atom : (info : SourceInfo) → (val : String) → motive_1 (Syntax.atom info val))
  (ident :
    (info : SourceInfo) →
      (rawVal : Substring) →
        (val : Name) → (preresolved : List Syntax.Preresolved) → motive_1 (Syntax.ident info rawVal val preresolved))
  (mk : (toList : List Syntax) → motive_3 toList → motive_2 { toList := toList }) (nil : motive_3 [])
  (cons : (head : Syntax) → (tail : List Syntax) → motive_1 head → motive_3 tail → motive_3 (head :: tail))
  (t : List Syntax) : motive_3 t

[Robin Arnez]

Well I think Meta.mkRecursorInfo is for custom recursors usable by the induction tactic and as you know, induction doesn't support mutual or nested inductives, so similarly Meta.mkRecursorInfo doesn't support them. Are you looking for docs#Lean.getConstInfoRec​?

[Leni Aniva]

Robin Arnez said:

Well I think Meta.mkRecursorInfo is for custom recursors usable by the induction tactic and as you know, induction doesn't support mutual or nested inductives, so similarly Meta.mkRecursorInfo doesn't support them. Are you looking for docs#Lean.getConstInfoRec​?

ah I see what you mean. I was just curious because this constant looks like a recursor.

[Robin Arnez]

I mean yeah, it is a recursor, but not one supported by docs#Lean.Meta.mkRecursorInfo which expects one motive only

[Kyle Miller]

Reading the code, this error ("invalid user defined recursor Syntax.rec_2, type of the major premise does not contain the recursor parameter") is caused by motive_1 and motive_2 not being able to be determined from the major premise or the return type. Robin's correct that this function is for the induction/cases tactics.

[Kyle Miller]

Actually, I take that back a little; it's for the meta tactics (like MVarId.induction), not the user-facing tactics. The induction/cases tactics use Lean.Meta.getElimInfo.