Showing the normal form of a type?

Stream: general

[Joey Eremondi]

I'm wondering, in Lean 4 is there a way to show a normal form of a type?

For example, in mathlib, CategoryTheory.Arrow is defined using CategoryTheory.Comma. I'm trying to create an object of type Arrow Type, but in the display window the goal is just shown as Arrow Type, so I have no idea how to actually construct a thing?

Is there a way to get the goal-display to unwrap the definitions? Or even just to get a hint as for how to proceed building a thing of the given type? In Agda I'd use "C-u C-u C-c Cd" to display the normalized goal, and I'd do "C-c c" or "C-c r" to refine or case-split the goal to tell how to actually build the thing. Is there an equivalent in Lean?

I tried#eval to unroll the definitions but it gave an error about Type not implementing MetaEval.

[Eric Wieser]

If you enter tactic mode, you could use unfold Arrow

[Eric Wieser]

For splitting the goal, typing a _ and clicking the lightbulb works (it has a key-shortcut but it might be platform dependent)

[Joey Eremondi]

Ooh, that's nice to know about the _, thanks

[Eric Wieser]

Though often a better strategy is to go to the definition of Arrow for examples of or API for constructing it

[Joey Eremondi]

Right, so I guess what I'm asking is, is there an in-editor workflow for this? Or do you just always have the editor open in one window and the browser open in the other with the API docs?

[Eric Wieser]

You can control-click on Arrow in the goal view to see its definition

[Eric Wieser]

Or in the source pane, or via whatever your keybinding is, etc

[Scott Morrison]

I use F12 (jump to definition) constantly. If you want to stay on the keyboard in tactic mode often typing constructor is helpful.

[Kyle Miller]

Mathlib has whnf and reduce tactics that reduce terms. whnf will unfold definitions at the head of a term, and reduce will reduce everything recursively (it's what #reduce gives you). These likely go much too far.