9 lines
253 B
Text
9 lines
253 B
Text
[Elab.step] #check fun x => m x
|
|
[Elab.step] none fun x => m x
|
|
[Elab.step] Sort _ _
|
|
[Elab.step] none m x
|
|
[Elab.step] none fun x✝ => x
|
|
[Elab.step] Sort _ _
|
|
[Elab.step] none x
|
|
fun (x : ?m) (x_1 : ?m x) => x : (x : ?m) → ?m x → ?m
|
|
[Elab.step] end
|