Documentation

Transfer.Synthesis.ParamResolve

The upward level search (param_resolve) #

The synthesizer (ParamSynth/ParamSynthExt) builds Param witnesses at a finite menu of registered levels; ParamWeaken downgrades a witness along the lattice. This module ties them into the level-directed resolver: a recursive tactic param_resolve that closes a Param m n A B goal at any target level reachable in the lattice, by

  1. trying a registered instance exactly at the goal's (m,n) (the fixed-menu synthesizer — handles the self-relation (map1,map1) and (map3,map0) arrows and leaves directly);
  2. else synthesizing at a stronger registered level and Param.weaken-ing down to the goal's (m,n) (the "synthesize-high, use-low" search — the ⊑ side conditions are discharged by decide);
  3. else decomposing an arrow (apply paramArrow) and recursing on the two components;
  4. else falling back to the embedding / equivalence leaves.

For the univalence-free fragment, witness synthesis is level-directed (any (m,n) ⊑ a synthesizable level, over arrow/base structure) rather than pinned to a fixed menu. The map4 universe relation remains unreachable — and, as UnivalenceStatus proves, necessarily so (UA is inconsistent in Lean). Beyond this lies the full term-level ⟦t⟧ over arbitrary (non-type-directed) terms — a separate, larger metaprogram.

source
def Transfer.Param.tacticParam_resolve :
Lean.ParserDescr

The level-directed resolver. Closes a Param m n A B goal at any lattice-reachable level. See the module docstring for the four strategies.

Equations
Instances For

    Demonstrations: level-directed resolution at multiple targets #

    Each goal is closed by param_resolve alone — the level is found, not supplied.