Term mode feels like an afterthought

Stream: new members

[Dan Abramov]

I know I'm probably thinking about it wrong (because in a way, terms are more fundamental) but whenever I'm in term mode, I feel like I'm fighting with the tool.

For example, say I got this:

Screenshot 2025-07-23 at 02.08.16.png

I need to unfold FunctionalRels at F to see "what it is" (what I'm given as its properties). But I can't unfold because unfold is a tactic mode thing.

Okay, I switch to tactic mode temporarily so that I can use unfold and peek at the definition in my InfoView:

Screenshot 2025-07-23 at 02.09.22.png

Ah, okay, that gives me an idea, I can unpack F:

Screenshot 2025-07-23 at 02.10.32.png

But wait, I wanted to write this thing in term mode, I'm not proving anything after all. Let me switch back to term mode:

Screenshot 2025-07-23 at 02.11.06.png

Right, I guess unfold isn't a thing, and obtain isn't a thing either. Let me fix that.

Screenshot 2025-07-23 at 02.11.35.png

Uhhh... So where's my p, hp1, and hp2? They're not showing up in InfoView at all!

Let me add another variable:

Screenshot 2025-07-23 at 02.12.29.png

Great, now they're showing up. So I always have to add "one more variable" and put the cursor at the line below just to make InfoView work in the term mode. In other words, in term mode, InfoView just casually disregards the last let before the sorry, whatever it is.

This workflow just doesn't feel very productive. Both in terms of inability to unfold, and in terms of InfoView being broken. And then you also have to remember that only a subset of tools I'm used to work there (let is cool, but obtain is not, etc).

All in all this just makes me always switch to tactic mode so that I don't have to deal with limited and/or broken tooling. Is that what other people do, too? Or do people switch back and forth all the time, reformatting it in term mode at the end? Or do people tolerate the brokenness of InfoView and lack of features in term mode? Or is term mode only used for simple things where you already know what you're planning to write?

I just feel like I'm using it wrong and I'm surprised that the workflow feels subpar compared to tactic mode. It feels like term mode is an afterthought but surely it can't be?

[Weiyi Wang]

I haven't finished reading the whole thing yet, but

But wait, I wanted to write this thing in term mode, I'm not proving anything after all. Let me switch back to term mode:

Here are a few things good to know

• It is fine to use tactic mode for non-proof def
• you can insert long terms in tactic mode in various places. The most basic one is exact <pretend you are back to term mode here>.

[Kenny Lau]

@Dan Abramov

1. you can convert to term mode after the whole tactic definition
2. where you put your cursor matters a lot in term mode. My trick is to always insert underscores (_) so that the whole thing is grammatical (and I never use sorry), and you always put the cursor to the left of the underscore and look at the expected type
3. and I hope you remember to destroy the let after the whole definition (by using projections instead) :slight_smile:

[Yakov Pechersky]

Dan, when in term mode, have you placed holes? _ For the final goal.

[Kenny Lau]

def foo (h : Nat × Nat × Nat) : Nat → Nat :=
  let ⟨x, hx⟩ := h
  _
--^ put cursor before

[Dan Abramov]

It is fine to use tactic mode for non-proof def

Acknowledged though I do feel a bit guilty doing that. The stylistic rule of thumb I'm imagining is to use tactic mode for proofs, and term mode for "exact" proofs or for function definitions. Maybe I should just let go of this and embrace tactic mode for everything?

where you put your cursor matters a lot in term mode. My trick is to always insert underscores (_) so that the whole thing is grammatical (and I never use sorry), and you always put the cursor to the left of the underscore and look at the expected type

Ok yea I can do that. It still seems like a bug that InfoView doesn't recognize let until next non-whitespace token but hopefully that gets fixed eventually. What surprised me more is that it almost feels like InfoView in term mode is neglected — I struggle to imagine a similar bug in tactic mode existing without driving people up the wall every day. So I suppose term mode is just used less?

and I hope you remember to destroy the let after the whole definition (by using projections instead) :slight_smile:

Say more! :D I don't know what this means.

[Kenny Lau]

@Dan Abramov it's not a bug, you should always put your cursor before an _, in some sense that's the only correct place to put your cursor

[Kenny Lau]

to me what the infoview says at any other place is Undocumented Behaviour

[Kenny Lau]

Dan Abramov said:

Say more! :D I don't know what this means.

def foo (h : Nat × Nat × Nat) : Nat → Nat :=
  let ⟨x, y⟩ := h
  fun r ↦ x

def foo' (h : Nat × Nat × Nat) : Nat → Nat :=
  fun r ↦ h.fst

[Kenny Lau]

the second is preferred over the first

[Dan Abramov]

to me what the infoview says at any other place is Undocumented Behaviour

Hmm I find that to be a very non-user-friendly stance. I think InfoView should show the same thing for these two positions:

Screenshot 2025-07-23 at 02.33.53.png

Screenshot 2025-07-23 at 02.34.02.png

But it doesn't.

[Dan Abramov]

the second is preferred over the first

Ah, do you mean it's preferred to extract common projections as top-level functions?

[Weiyi Wang]

Maybe I should just let go of this and embrace tactic mode for everything?

As someone who is also not good at term mode, I switch to tactics whenever I feel drowned in terms, and then do a clean up after I finish building the proof/def to fold tactics into terms if I feel like it.

Similar to having terms in tactic mode, you can also have small tactics partially in term mode, like def foo := func x y (by ...) z. When you are doing early drafting, feel free to interleave them whenever you feel like it

[Dan Abramov]

OK makes sense so maybe tactic mode just offers a better workflow, and then during cleanup it might make sense to collapse the result into term mode for terseness and simplicity.

[Yakov Pechersky]

Kenny Lau said:

Dan Abramov said:

Say more! :D I don't know what this means.

def foo (h : Nat × Nat × Nat) : Nat → Nat :=
  let ⟨x, y⟩ := h
  fun r ↦ x

def foo' (h : Nat × Nat × Nat) : Nat → Nat :=
  fun r ↦ h.fst

I'm not sure that's true anymore. It was true in Lean3, but in Lean4, we have defeq eta expansion, and the two are the same.

[Kenny Lau]

there is also another suboptimal point about your workflow: you shouldn't have to unfold anything, you should be able to click "go to the definition" and (very crucially!) the "API" should just be below the definition

(API means the set of definitions and lemmas that allow you to use the definition in its intended way)

[Yakov Pechersky]

Although I guess #print foo has the naked match in the term.

[Kenny Lau]

Yakov Pechersky said:

and the two are the same.

def foo (h : Nat × Nat × Nat) : Nat → Nat :=
  let ⟨x, y⟩ := h
  fun r ↦ x

def foo' (h : Nat × Nat × Nat) : Nat → Nat :=
  fun r ↦ h.fst

theorem bar (p : Nat × Nat × Nat) (h : p.fst = 3) : foo p 1 = 3 := by
  unfold foo
  rw [h]

theorem bar' (p : Nat × Nat × Nat) (h : p.fst = 3) : foo' p 1 = 3 := by
  unfold foo'
  rw [h]

[Yakov Pechersky]

def foo (h : Nat × Nat × Nat) : Nat → Nat :=
  let ⟨x, y⟩ := h
  fun r ↦ x

def foo' (h : Nat × Nat × Nat) : Nat → Nat :=
  fun r ↦ h.fst

example (h : Nat × Nat × Nat) : foo h = foo' h := rfl

[Kenny Lau]

yes, but rw doesn't work up to rfl :slight_smile:

[Dan Abramov]

there is also another suboptimal point about your workflow: you shouldn't have to unfold anything, you should be able to click "go to the definition" and (very crucially!) the "API" should just be below the definition

Well, the problem is that by the time I navigate to definition, I've forgotten the context of what I was trying to do. I literally rely on InfoView to think. Maybe that's part of the problem but my mental faculties are limited and I try not to waste them on what tooling can do for me.

[Kyle Miller]

With terms, I think it's important to remember that now it's Just Programming and you need to be doing whatever you normally do to write good programs. Relying too much on unfolding types makes programming difficult to follow — maybe FunctionalRels.Elem is missing some helper functions?

[Kyle Miller]

Lean term trick: if you want to drop back into tactics to do some exploration midway through some terms, you can insert a line like

have : True := by ...

[Dan Abramov]

Ok so maybe a good workflow is

• Use tactic mode for exploration
• Extract chunks of exploration into helper lemmas and projections
• See if the rest becomes simple enough for term mode

[Kyle Miller]

(It would be neat if the Infoview had some exploratory mode where you could unfold things and do various other reductions step-by-step!)

[Johan Commelin]

@Dan Abramov Fwiw, there is also the show_term {more tactics go here} tactic, that show you the term that a tactic constructs.

[Dan Abramov]

Broadly speaking, is unfold an anti-pattern outside exploration phase? Should I be creating lemmas to avoid unfolding definitions?

[Julian Berman]

Yes, using unfold is peeking at implementation details anywhere that does it, and writing lemmas is like instead declaring some public API and then using that, even if it just delegates to the same implementation details by saying the proof is rfl or whatever. (But then later if those change, nothing breaks as long as the public API all stayed the same)

[suhr]

Dan Abramov said:

Broadly speaking, is unfold an anti-pattern outside exploration phase?

Think more broadly: you don't just use unfold, you also do some simplifications to unfolded expressions. Since you have to derive intermediate results anyway, why not move them into separate lemmas? This also would make proofs less sensitive to implementation details.

[Marc Huisinga]

Regarding the "Expected type is not helpful on whitespace" issue: I think this is partly due to the fact that the expected type TermInfo selection is using the same logic as the one for hovers, and not much thought has been given to what should be done in whitespace. Without having looked into it too deeply, in:

example : True :=
  let a := 1
  let b := 2
  -- <cursor>
  sorry

it seems to pick the one for let b := 2; sorry (since that one includes the cursor in its range), which obviously doesn't have b in its context yet.
The tactic goal states work very differently.

This probably doesn't get noticed that much by most users because they have been trained to work with _ since the Lean 3 days.

@Dan Abramov could you create a bug report for this in the Lean 4 repo? I don't think this has a quick fix.

[Dan Abramov]

Thanks, filed https://github.com/leanprover/lean4/issues/9492

[Dan Abramov]

Fascinating, I've started reworking a proof I was completely stuck on while trying to follow these guidelines (no unfolding) and it completely changed my process. It's forced me to rethink the building pieces (and make some abstractions explicit), and the value of that was higher than I expected.

In programming, extracting things is usually much lower value (I tend to avoid extracting pieces until I'm sure I need to reuse them). But here something is different.

[Dan Abramov]

I'm guessing in programming the abstraction boundaries are harder to pierce by default so you're kind of forced to deal with them anyway. Whereas Lean is more lax about it which is handy in some ways but led me to rely on it too much.