isProjectionFn for propositional fields

Stream: metaprogramming / tactics

[Chase Norman]

structure Test where
  non_prop: Unit
  prop: True

In this code snippet, non_prop is considered a projection function by the environment and prop is not. I understand that this is because these fields are compiled out. However, I would still like to know the name of the structure type and the field index of these fields. Is there a way to do this?

[Aaron Liu]

What do you mean?

import Lean

structure Test where
  non_prop: Unit
  prop: True

/--
info: true
-/
#guard_msgs in
run_elab do
  let b ← Lean.isProjectionFn ``Test.non_prop
  IO.println b

/--
info: true
-/
#guard_msgs in
run_elab do
  let b ← Lean.isProjectionFn ``Test.prop
  IO.println b

[Chase Norman]

Ah, thank you very much, I see my mistake. I was first checking that the symbol was a definition before checking if it was a projection. In this case, the symbol is a theorem, not a definition.

Adding to my embarrassment, may I ask how you are seeing the output of IO.println? Running lake build I don't see anything in my terminal, output, or debug console. I even tried using dbg_trace to see something in the infoview, but to no avail.

[Aaron Liu]

I was using the web server

[Aaron Liu]

Also, #guard_msgs is suppressing the messages.