Design: isAlwaysSpecified returns true for all declaration kinds

[astefano]

Description

In ProbeLean/Specify.lean, isAlwaysSpecified returns true for every DeclKind variant:

def isAlwaysSpecified (kind : DeclKind) : Bool :=
  match kind with
  | .theorem => true
  | .class => true
  | .structure => true
  | .inductive => true
  | .instance => true
  | .axiom => true
  | .def => true
  | .abbrev => true
  | .opaque => true
  | .quot => true

This makes the specified field in specs output always true, rendering it semantically meaningless.

Question

Is this intentional for Lean (since every declaration has a type signature by construction)? If so, it should be documented. If not, what should the actual semantics be? For example, should def without a docstring or explicit spec be considered unspecified?