structure with no fields is not a structure

Stream: metaprogramming / tactics

[Eric Wieser]

I found this surprising:

structure no_fields : Type

run_cmd do
  e ← tactic.get_env,
  tactic.trace (e.is_structure `no_fields)
-- ff

[Kyle Miller]

I haven't checked if it's calling the same function, but I remember is_structure at https://github.com/leanprover-community/lean/blob/master/src/frontends/lean/structure_cmd.cpp#L118 being more complicated than I would have expected

[Eric Wieser]

Looks like it deliberately considers structures with no fields as not structures: https://github.com/leanprover-community/lean/blob/9d5adc6ab80d02bb2a0fd39a786aaeb1efd6fb01/src/frontends/lean/structure_cmd.cpp#L129

[Eric Wieser]

That feels like it could just be a bug

[Mario Carneiro]

I vote for considering this a bug

[Mario Carneiro]

Lean 4 agrees:

import Lean

structure Foo

open Lean
#eval show MetaM _ from do
  dbg_trace "{isStructure (← getEnv) ``Foo}"
  -- true

[Eric Wieser]

Attempted as leanprover-community/lean#739

[Eric Wieser]

CI seems not to care