blob: fb7ec6f25be8e3916994d83391c9290122498bec [file] [edit]
fun x x_1 => x : (x : ?m) → ?m x → ?m
[Elab.step] expected type: <not-available>, term
fun x => m x
[Elab.step] expected type: Sort ?u, term
_
[Elab.step.result] ?m
[Elab.step] expected type: <not-available>, term
m x
[Elab.step] expected type: <not-available>, term
fun x✝ => x
[Elab.step] expected type: Sort ?u, term
_
[Elab.step.result] ?m
[Elab.step] expected type: <not-available>, term
x
[Elab.step.result] x
[Elab.step.result] fun x_1 => x
[Elab.step.result] fun x_1 => x
[Elab.step.result] fun x x_1 => x