Lean.isBRecOnRecursor false for inductive predicates in Prop

Stream: lean4

[Joachim Breitner]

I stumbled over docs#Lean.isBRecOnRecursor being false for the .brecOn of Prop-valued induction principles:

import Lean.Elab.Command

/-- info: false -/
#guard_msgs in
run_meta Lean.logInfo m!"{Lean.isBRecOnRecursor (← Lean.getEnv) ``Acc.brecOn}"

namespace IndProp

inductive Even : Nat → Prop where
| zero : Even 0
| plus2 : Even n → Even (n + 2)

/-- info: false -/
#guard_msgs in
run_meta Lean.logInfo m!"{Lean.isBRecOnRecursor (← Lean.getEnv) ``Even.brecOn}"

end IndProp

namespace NonProp
inductive Even : Nat → Type where
| zero : Even 0
| plus2 : Even n → Even (n + 2)

/-- info: true -/
#guard_msgs in
run_meta Lean.logInfo m!"{Lean.isBRecOnRecursor (← Lean.getEnv) ``Even.brecOn}"

end NonProp

Is there a good reason for this being false?

And how can that even be? I see that the construction function for brecOn in
https://github.com/leanprover/lean4/blob/655ec964f5d6b0810ce0e517a6b3bbb3d5186d25/src/library/constructions/brec_on.cpp#L159-L351
ends with

    new_env = add_aux_recursor(new_env, brec_on_name);

(which should set the “is aux recursor” attribute checked by isBRecOnRecursor), so how comes that there even exists a brecOn definition without that attribute?

Or put differently: Since that function starts with

static environment mk_brec_on(environment const & env, name const & n, bool ind) {
    if (!is_recursive_datatype(env, n))
        return env;
    if (is_inductive_predicate(env, n))
        return env;

it doesn't seem to be the one generating Acc.brecOn, but then who does?

[Arthur Adjedj]

it doesn't seem to be the one generating Acc.brecOn, but then who does?

I believe the magic happens at the elaborator level for inductive predicates, not in the cpp libraries: https://github.com/leanprover/lean4/blob/655ec964f5d6b0810ce0e517a6b3bbb3d5186d25/src/Lean/Meta/IndPredBelow.lean#L576-L577

[Joachim Breitner]

Thanks! That answers half the question.

Now I wonder if anything would break if these brecOn's also get that attribute set.