Getting the goal in infoview as a string

Stream: lean4

[Roozbeh Yousefzadeh]

Hello,
I am new here. I am trying to get the information in the infoview as a string. Is there an easy way to do this using the Lean language and within the Lean environment? In the infoview, I'm only interested in the goals.

I would guess methods such as Linarith, simp, exact?, and apply? also extract the current goal as a string and then work on the string. Is that so? Where can I find the implementation of exact? and apply? ?

[Kim Morrison]

No, nothing uses String representations of the goal.

[Kim Morrison]

The implementation of exact? is at https://github.com/leanprover/lean4/blob/master/src/Lean/Elab/Tactic/LibrarySearch.lean and imports thereof.

[Kim Morrison]

You might find the Lean metaprogramming book a reasonable place to start to learn how to manipulate goals programmatically.

[Roozbeh Yousefzadeh]

Thank you for your helpful response.

[Roozbeh Yousefzadeh]

If I were to calculate the length of my current goal (i.e., just knowing how many characters there are in the current goal), is there a way to do that within lean?

[Kim Morrison]

e.g.

open Lean Lean.Elab.Tactic Lean.Meta
example : 1 + 1 = 2 := by
  run_tac do
    let g ← getMainTarget
    let s ← ppExpr g
    logInfo s!"{(toString s).length}"
  rfl

[Roozbeh Yousefzadeh]

Perfect, thanks. I can now build on this function doing more sophisticated calculations.

The meta programming book is great. I came across the TacticM and Lean.saveState.

I am trying to develop an automatic system for proving theorems.