K-like inductives don't take arguments

Stream: general

[Mario Carneiro]

@Gabriel Ebner I just discovered by reading the source code that lean doesn't consider an inductive suitable for K-like reduction unless it has 0 arguments in the constructor, rather than having all arguments in the output type like I thought (and wrote in my paper). Do you know why this is?

inductive  eq' {α} : α → α →  Prop
| refl : ∀ a, eq' a a
variables {α : Sort*} {C : α → α → Sort*}
(e : ∀ (a : α), C a a) (a : α) (h : eq' a a)
#reduce  @eq'.rec α C e a a h --expected: e a

[Gabriel Ebner]

The purpose of K-like reduction is that eq and heq reduce better. And "single constructor with no arguments" is the easiest criterion for that. IIRC, the code even constructs an explicit eq.refl/heq.refl/etc. term and checks whether it is def-eq with the major premise during reduction.