Module common 

Functions

entry_basename

Basename for the entry file emitted by Lean / Dafny. Prefer the source-declared module name (module Foo → Foo) so the entry file’s name matches what the user wrote; fall back to a capitalised project name when no module declaration is present. Lake’s path-as-module-name convention forces this for Lean — Dafny doesn’t strictly need it but the same basename keeps the two backends aligned (no more playground.dfy vs OracleTrace.lean).

is_pure_fn

A function is pure if it declares no effects and isn’t main.

is_recursive_product

Granular variant of is_recursive_type_def for products.

is_recursive_sum

Granular variant of is_recursive_type_def taking a sum’s (name, variants) split — some backends already have the parts separated and don’t want to rebuild a TypeDef just to query.

is_recursive_type_def

True when the type definition mentions its own name somewhere in a field or variant payload (recursive ADT).

type_def_name

The declared name of a type definition.