what are modes?

Stream: new members

[rzeta0]

After 2 weeks of starting to work through beginner tutorials - I am still not clear what a mode is?

Tactic mode. Calc mode. Term mode. Conv mode?

Is there a simple way of explaining what they are and they even exist?

[František Silváši 🦉]

All proofs are terms.
Modes are different kinds of ways to construct these terms.

Term mode lets you input terms directly.
Tactic mode lets you call tactics which end up generating terms programatically.
There are also calc and conv, they're a bit more specific.
Calc mode lets you chain transitive relations. Conv mode lets you focus on various parts of terms.

Why do they exist?
Because they are more convenient to express proofs in.

[Jon Eugster]

I am not an expert when it comes to using the correct words/terms, but I'd say that the word "mode" is more colloquial rather than a concept that's clearly distinct from the notion of a term. In technical terms they might be more like different Parsers:

Your proof (a-priori a string of symbols in your text file) is parsed into one big term and there are different rules on how to parse this. by, calc, conv, etc. are all of these kind, for example by is defined as

def byTactic : Parser := leading_parser:leadPrec
  ppAllowUngrouped >> "by " >> Tactic.tacticSeqIndentGt

which essentially says 'after you see the string "by " you should parse the stuff afterwards as indented tactic sequence'.
and creating this tactic sequence is what we call "Tactic mode".

Or calc is defined this way:

syntax calcStep := ppIndent(colGe term " := " term)
syntax calcSteps := ppLine withPosition(calcFirstStep) withPosition((ppLine linebreak calcStep)*)
syntax (name := calc) "calc" calcSteps : term

So calc is followed by a calcSteps sequence and each of these steps is of the form term " := " term. So "calc mode" is somehow being inside the constructing of such a calc-step sequence.

(Lean then elaborates these terms into Expressions, where it can also do stuff like having holes (aka open goals) and checking types which it then uses to feedback you the interactive stuff you see in the infoview)

[rzeta0]

thanks Jon - the insight that these keywords trigger different parsing is helpful