Lean4
/-- Elaborator for sections in a fibre bundle: converts a section `s : Π x : M, V x` as a dependent
function to a non-dependent function into the total space. This handles the cases of
- sections of a trivial bundle
- vector fields on a manifold (i.e., sections of the tangent bundle)
- sections of an explicit fibre bundle
- turning a bare function `E → E'` into a section of the trivial bundle `Bundle.Trivial E E'`
This elaborator searches the local context for suitable hypotheses for the above cases by matching
on the expression structure, avoiding `isDefEq`. Therefore, it is (hopefully) fast enough to always
run.
-/
-- TODO: document how this elaborator works, any gotchas, etc.
-- TODO: factor out `MetaM` component for reuse
@[scoped term_parser 1000]
public meta def «termT%_» : Lean.ParserDescr✝ :=
ParserDescr.node✝ `Manifold.«termT%_» 1024
(ParserDescr.binary✝ `andthen (ParserDescr.symbol✝ "T% ") (ParserDescr.cat✝ `term 1023))
