`isClass?` returns none for instances proving structure predicates like `Continuous`, causing panic

[NicolasRouquette]

doc-gen4 panics when processing certain instances where isClass? returns none. This occurs for instances that prove structure predicates rather than class instances.

Minimal Working Example

See: https://github.com/NicolasRouquette/ClassFieldTheory/blob/bug/doc-gen4/isClass/MWE_isClass.lean

The problematic instance is here: ClassFieldTheory.LocalCFT.Continuity.continuous_algebraMap_of_density:

/-- Maddy's Lemma : Density implies continuity. -/
@[fun_prop] instance continuous_algebraMap_of_density :
    Continuous (algebraMap K L) := ...

Root Cause

The issue is that Continuous is a structure (a Prop predicate), not a class:

structure Continuous (f : X → Y) : Prop where ...

When isClass? is called on the type of an instance that proves Continuous f, it correctly returns none because Continuous is not registered as a class in the environment.

Current Behavior

In InstanceInfo.ofDefinitionInfo, doc-gen4 calls:

let some className ← Meta.isClass? type
  | panic! s!"isClass? returned none for instance {info.name}"

This panics for instances like continuous_algebraMap_of_density.

Expected Behavior

doc-gen4 should handle isClass? returning none gracefully, either by:

• Generalize doc-gen4 to handle instances of classes or structures
• Returning none from ofDefinitionInfo (changing return type to Option InstanceInfo)
• Skipping these instances during documentation generation
• Logging a warning instead of panicking

MWE Output

Running the MWE shows:

Constant: continuous_algebraMap_of_density
isClass? returned: none
⚠️  This is the bug! doc-gen4 panics when isClass? returns none for an instance.

--- Analyzing the type structure ---
Head function: Continuous
Head is constant: Continuous
✗ Continuous is NOT registered as a class

Constant: instAddNat
isClass? returned: some Add
✓ Add is registered as a class

Environment

• Lean: 4.27.0-rc1
• doc-gen4: latest main branch
• Project: ClassFieldTheory (branch bug/doc-gen4/isClass)