Module detect 

Proof-mode recursion classifier.

Backend-neutral pattern matching over the Aver AST that decides, for each recursive pure fn (or mutual-recursion SCC), which RecursionPlan variant applies — or emits a ProofModeIssue when the shape falls outside the supported set.

Lean and Dafny consume the same plans through crate::codegen::recursion::analyze_plans; a couple of helpers that depend on AST queries tied to Lean’s toplevel (pure-fn predicate, recursive-type-def predicate, type-def name) still live in crate::codegen::lean and are re-used here through pub(crate) exports. That could move to a neutral AST helper module in a later pass.

Functions

analyze_plans

Classify every recursive pure fn in ctx. The returned map assigns each supported function a RecursionPlan; anything that falls outside the recognised shapes becomes a ProofModeIssue.