Supporting results for pointwise provable equality.

def PointwiseComposition.Lean.TSyntax.freshIdent {m : Type → Type} [Monad m] [Lean.MonadQuotation m] : m (Lean.TSyntax `ident)

The fresh Ident construction in Lean.TSyntax.

Equations

• PointwiseComposition.Lean.TSyntax.freshIdent = do let name ← Lean.Elab.Term.mkFreshBinderName pure { raw := (Lean.mkIdent name).raw }

@[reducible, inline]

abbrev PointwiseComposition.FFL.FirstOrder.BinderNotation.finSuccItr {n : ℕ} (i : Fin n) (m : ℕ) : Fin (n + m)

The fin Succ Itr construction in FFL.FirstOrder.BinderNotation.

Equations

• PointwiseComposition.FFL.FirstOrder.BinderNotation.finSuccItr i 0 = i
• PointwiseComposition.FFL.FirstOrder.BinderNotation.finSuccItr i m.succ = (PointwiseComposition.FFL.FirstOrder.BinderNotation.finSuccItr i m).succ

(Literal) Notation for terms

def Lean.Parser.Category.firstOrderTerm : Category

The first order term construction in Lean.Parser.Category.

Equations

• Lean.Parser.Category.firstOrderTerm = { }

def PointwiseComposition.FFL.FirstOrder.BinderNotation.firstOrderTerm.quot : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Lean.Parser.Category.firstOrder.quoteType : Category

The quote type construction in Lean.Parser.Category.first_order.

Equations

• Lean.Parser.Category.firstOrder.quoteType = { }

def PointwiseComposition.FFL.FirstOrder.BinderNotation.firstOrder.quoteType.quot : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def PointwiseComposition.FFL.FirstOrder.BinderNotation.quoteTypeLit : Lean.ParserDescr

The quote type Lit construction in FFL.FirstOrder.BinderNotation.

Equations

• PointwiseComposition.FFL.FirstOrder.BinderNotation.quoteTypeLit = Lean.ParserDescr.node `PointwiseComposition.FFL.FirstOrder.BinderNotation.quoteTypeLit 1024 (Lean.ParserDescr.symbol "lit")

def PointwiseComposition.FFL.FirstOrder.BinderNotation.quoteTypeFaf : Lean.ParserDescr

The quote type Faf construction in FFL.FirstOrder.BinderNotation.

Equations

• PointwiseComposition.FFL.FirstOrder.BinderNotation.quoteTypeFaf = Lean.ParserDescr.node `PointwiseComposition.FFL.FirstOrder.BinderNotation.quoteTypeFaf 1024 (Lean.ParserDescr.symbol "faf")

def PointwiseComposition.FFL.FirstOrder.BinderNotation.«termQuoteterm(_)[_|_|_]» : Lean.ParserDescr

The «term Quoteterm( )[ | | ]» construction in FFL.FirstOrder.BinderNotation.

Equations

• One or more equations did not get rendered due to their size.

def PointwiseComposition.FFL.FirstOrder.BinderNotation.«firstOrderTerm(_)» : Lean.ParserDescr

The «first order term( )» construction in FFL.FirstOrder.BinderNotation.

Equations

• One or more equations did not get rendered due to their size.

def PointwiseComposition.FFL.FirstOrder.BinderNotation.firstOrderTerm_ : Lean.ParserDescr

The first order term construction in FFL.FirstOrder.BinderNotation.

Equations

• One or more equations did not get rendered due to their size.

def PointwiseComposition.FFL.FirstOrder.BinderNotation.«firstOrderTerm#_» : Lean.ParserDescr

The «first order term# » construction in FFL.FirstOrder.BinderNotation.

Equations

• One or more equations did not get rendered due to their size.

def PointwiseComposition.FFL.FirstOrder.BinderNotation.«firstOrderTerm&_» : Lean.ParserDescr

The «first order term& » construction in FFL.FirstOrder.BinderNotation.

Equations

• One or more equations did not get rendered due to their size.

def PointwiseComposition.FFL.FirstOrder.BinderNotation.«firstOrderTerm!__⋯» : Lean.ParserDescr

The «first order term! ⋯» construction in FFL.FirstOrder.BinderNotation.

Equations

• One or more equations did not get rendered due to their size.

def PointwiseComposition.FFL.FirstOrder.BinderNotation.firstOrderTerm!!_ : Lean.ParserDescr

The first order term!! construction in FFL.FirstOrder.BinderNotation.

Equations

• One or more equations did not get rendered due to their size.

def PointwiseComposition.FFL.FirstOrder.BinderNotation.«firstOrderTerm.!__⋯» : Lean.ParserDescr

The ! ⋯» construction in FFL.FirstOrder.BinderNotation.«firstOrderTerm.

Equations

• One or more equations did not get rendered due to their size.

def PointwiseComposition.FFL.FirstOrder.BinderNotation.«firstOrderTerm.!!_» : Lean.ParserDescr

The !! » construction in FFL.FirstOrder.BinderNotation.«firstOrderTerm.

Equations

• One or more equations did not get rendered due to their size.

def PointwiseComposition.FFL.FirstOrder.BinderNotation.firstOrderTerm__1 : Lean.ParserDescr

The first order term 1 construction in FFL.FirstOrder.BinderNotation.

Equations

• One or more equations did not get rendered due to their size.

def PointwiseComposition.FFL.FirstOrder.BinderNotation.«firstOrderTerm↑_» : Lean.ParserDescr

The «first order term↑ » construction in FFL.FirstOrder.BinderNotation.

Equations

• One or more equations did not get rendered due to their size.

def PointwiseComposition.FFL.FirstOrder.BinderNotation.«firstOrderTerm⋆» : Lean.ParserDescr

The «first order term⋆» construction in FFL.FirstOrder.BinderNotation.

Equations

• One or more equations did not get rendered due to their size.

def PointwiseComposition.FFL.FirstOrder.BinderNotation.«firstOrderTerm_+_» : Lean.TrailingParserDescr

The «first order term + » construction in FFL.FirstOrder.BinderNotation.

Equations

• One or more equations did not get rendered due to their size.

def PointwiseComposition.FFL.FirstOrder.BinderNotation.«firstOrderTerm_*_» : Lean.TrailingParserDescr

The «first order term * » construction in FFL.FirstOrder.BinderNotation.

Equations

• One or more equations did not get rendered due to their size.

def PointwiseComposition.FFL.FirstOrder.BinderNotation.«firstOrderTerm_^_» : Lean.TrailingParserDescr

The «first order term ^ » construction in FFL.FirstOrder.BinderNotation.

Equations

• One or more equations did not get rendered due to their size.

def PointwiseComposition.FFL.FirstOrder.BinderNotation.«firstOrderTerm_^'_» : Lean.TrailingParserDescr

The «first order term ^' » construction in FFL.FirstOrder.BinderNotation.

Equations

• One or more equations did not get rendered due to their size.

def PointwiseComposition.FFL.FirstOrder.BinderNotation.«firstOrderTerm_²» : Lean.TrailingParserDescr

The «first order term ²» construction in FFL.FirstOrder.BinderNotation.

Equations

• One or more equations did not get rendered due to their size.

def PointwiseComposition.FFL.FirstOrder.BinderNotation.«firstOrderTerm_³» : Lean.TrailingParserDescr

The «first order term ³» construction in FFL.FirstOrder.BinderNotation.

Equations

• One or more equations did not get rendered due to their size.

def PointwiseComposition.FFL.FirstOrder.BinderNotation.«firstOrderTerm_⁴» : Lean.TrailingParserDescr

The «first order term ⁴» construction in FFL.FirstOrder.BinderNotation.

Equations

• One or more equations did not get rendered due to their size.

def PointwiseComposition.FFL.FirstOrder.BinderNotation.«firstOrderTerm⌜_⌝» : Lean.ParserDescr

The «first order term⌜ ⌝» construction in FFL.FirstOrder.BinderNotation.

Equations

• One or more equations did not get rendered due to their size.

def PointwiseComposition.FFL.FirstOrder.BinderNotation.firstOrderTermExp_ : Lean.ParserDescr

The first order term Exp construction in FFL.FirstOrder.BinderNotation.

Equations

• One or more equations did not get rendered due to their size.

def PointwiseComposition.FFL.FirstOrder.BinderNotation.«term‘_’» : Lean.ParserDescr

The «term‘ ’» construction in FFL.FirstOrder.BinderNotation.

Equations

• One or more equations did not get rendered due to their size.

def PointwiseComposition.FFL.FirstOrder.BinderNotation.«term‘_|_’» : Lean.ParserDescr

A term with free variables.

Equations

• One or more equations did not get rendered due to their size.

def PointwiseComposition.FFL.FirstOrder.BinderNotation.«term‘_._’» : Lean.ParserDescr

A term with bound variables.

Equations

• One or more equations did not get rendered due to their size.

def PointwiseComposition.FFL.FirstOrder.BinderNotation.unexpanderNatLit : Lean.PrettyPrinter.Unexpander

The unexpander Nat Lit construction in FFL.FirstOrder.BinderNotation.

Equations

• One or more equations did not get rendered due to their size.

def PointwiseComposition.FFL.FirstOrder.BinderNotation.unexpanderOperatorConst : Lean.PrettyPrinter.Unexpander

The unexpander Operator Const construction in FFL.FirstOrder.BinderNotation.

Equations

• One or more equations did not get rendered due to their size.

def PointwiseComposition.FFL.FirstOrder.BinderNotation.unexpanderAdd : Lean.PrettyPrinter.Unexpander

The unexpander Add construction in FFL.FirstOrder.BinderNotation.

Equations

• One or more equations did not get rendered due to their size.

def PointwiseComposition.FFL.FirstOrder.BinderNotation.unexpanderMul : Lean.PrettyPrinter.Unexpander

The unexpander Mul construction in FFL.FirstOrder.BinderNotation.

Equations

• One or more equations did not get rendered due to their size.

def PointwiseComposition.FFL.FirstOrder.BinderNotation.unexpandFuncArith : Lean.PrettyPrinter.Unexpander

The unexpand Func Arith construction in FFL.FirstOrder.BinderNotation.

Equations

• One or more equations did not get rendered due to their size.

def PointwiseComposition.FFL.FirstOrder.BinderNotation.unexpandNumeral : Lean.PrettyPrinter.Unexpander

The unexpand Numeral construction in FFL.FirstOrder.BinderNotation.

Equations

• One or more equations did not get rendered due to their size.

Notation for formulae

def PointwiseComposition.FFL.FirstOrder.BinderNotation.firstOrderFormula.quot : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Lean.Parser.Category.firstOrderFormula : Category

The first order formula construction in Lean.Parser.Category.

Equations

• Lean.Parser.Category.firstOrderFormula = { }

def PointwiseComposition.FFL.FirstOrder.BinderNotation.«termQuoteformula(_)[_|_|_]» : Lean.ParserDescr

The «term Quoteformula( )[ | | ]» construction in FFL.FirstOrder.BinderNotation.

Equations

• One or more equations did not get rendered due to their size.

def PointwiseComposition.FFL.FirstOrder.BinderNotation.«firstOrderFormula(_)» : Lean.ParserDescr

The «first order formula( )» construction in FFL.FirstOrder.BinderNotation.

Equations

• One or more equations did not get rendered due to their size.

def PointwiseComposition.FFL.FirstOrder.BinderNotation.«firstOrderFormulaOf_term[_]» : Lean.ParserDescr

The «first order formula Of term[ ]» construction in FFL.FirstOrder.BinderNotation.

Equations

• One or more equations did not get rendered due to their size.

def PointwiseComposition.FFL.FirstOrder.BinderNotation.«firstOrderFormula!__⋯» : Lean.ParserDescr

The «first order formula! ⋯» construction in FFL.FirstOrder.BinderNotation.

Equations

• One or more equations did not get rendered due to their size.

def PointwiseComposition.FFL.FirstOrder.BinderNotation.firstOrderFormula!!_ : Lean.ParserDescr

The first order formula!! construction in FFL.FirstOrder.BinderNotation.

Equations

• One or more equations did not get rendered due to their size.

def PointwiseComposition.FFL.FirstOrder.BinderNotation.«firstOrderFormula.!__⋯» : Lean.ParserDescr

The ! ⋯» construction in FFL.FirstOrder.BinderNotation.«firstOrderFormula.

Equations

• One or more equations did not get rendered due to their size.

def PointwiseComposition.FFL.FirstOrder.BinderNotation.«firstOrderFormula.!!_» : Lean.ParserDescr

The !! » construction in FFL.FirstOrder.BinderNotation.«firstOrderFormula.

Equations

• One or more equations did not get rendered due to their size.

def PointwiseComposition.FFL.FirstOrder.BinderNotation.«firstOrderFormula⊤» : Lean.ParserDescr

The «first order formula⊤» construction in FFL.FirstOrder.BinderNotation.

Equations

• One or more equations did not get rendered due to their size.

def PointwiseComposition.FFL.FirstOrder.BinderNotation.«firstOrderFormula⊥» : Lean.ParserDescr

The «first order formula⊥» construction in FFL.FirstOrder.BinderNotation.

Equations

• One or more equations did not get rendered due to their size.

def PointwiseComposition.FFL.FirstOrder.BinderNotation.«firstOrderFormula_∧_» : Lean.TrailingParserDescr

The «first order formula ∧ » construction in FFL.FirstOrder.BinderNotation.

Equations

• One or more equations did not get rendered due to their size.

def PointwiseComposition.FFL.FirstOrder.BinderNotation.«firstOrderFormula_∨_» : Lean.TrailingParserDescr

The «first order formula ∨ » construction in FFL.FirstOrder.BinderNotation.

Equations

• One or more equations did not get rendered due to their size.

def PointwiseComposition.FFL.FirstOrder.BinderNotation.«firstOrderFormula¬_» : Lean.ParserDescr

The «first order formula¬ » construction in FFL.FirstOrder.BinderNotation.

Equations

• One or more equations did not get rendered due to their size.

def PointwiseComposition.FFL.FirstOrder.BinderNotation.«firstOrderFormula_→_» : Lean.TrailingParserDescr

The «first order formula → » construction in FFL.FirstOrder.BinderNotation.

Equations

• One or more equations did not get rendered due to their size.

def PointwiseComposition.FFL.FirstOrder.BinderNotation.«firstOrderFormula_↔_» : Lean.TrailingParserDescr

The «first order formula ↔ » construction in FFL.FirstOrder.BinderNotation.

Equations

• One or more equations did not get rendered due to their size.

def PointwiseComposition.FFL.FirstOrder.BinderNotation.«firstOrderFormula⋀_,_» : Lean.ParserDescr

The «first order formula⋀ , » construction in FFL.FirstOrder.BinderNotation.

Equations

• One or more equations did not get rendered due to their size.

def PointwiseComposition.FFL.FirstOrder.BinderNotation.«firstOrderFormula⋁_,_» : Lean.ParserDescr

The «first order formula⋁ , » construction in FFL.FirstOrder.BinderNotation.

Equations

• One or more equations did not get rendered due to their size.

def PointwiseComposition.FFL.FirstOrder.BinderNotation.«firstOrderFormula⋀_<_,_» : Lean.ParserDescr

The «first order formula⋀ < , » construction in FFL.FirstOrder.BinderNotation.

Equations

• One or more equations did not get rendered due to their size.

def PointwiseComposition.FFL.FirstOrder.BinderNotation.«firstOrderFormula⋁_<_,_» : Lean.ParserDescr

The «first order formula⋁ < , » construction in FFL.FirstOrder.BinderNotation.

Equations

• One or more equations did not get rendered due to their size.

def PointwiseComposition.FFL.FirstOrder.BinderNotation.«firstOrderFormula∀_,_» : Lean.ParserDescr

The «first order formula∀ , » construction in FFL.FirstOrder.BinderNotation.

Equations

• One or more equations did not get rendered due to their size.

def PointwiseComposition.FFL.FirstOrder.BinderNotation.«firstOrderFormula∃_,_» : Lean.ParserDescr

The «first order formula∃ , » construction in FFL.FirstOrder.BinderNotation.

Equations

• One or more equations did not get rendered due to their size.

def PointwiseComposition.FFL.FirstOrder.BinderNotation.«firstOrderFormula∀¹_» : Lean.ParserDescr

The «first order formula∀¹ » construction in FFL.FirstOrder.BinderNotation.

Equations

• One or more equations did not get rendered due to their size.

def PointwiseComposition.FFL.FirstOrder.BinderNotation.«firstOrderFormula∃¹_» : Lean.ParserDescr

The «first order formula∃¹ » construction in FFL.FirstOrder.BinderNotation.

Equations

• One or more equations did not get rendered due to their size.

def PointwiseComposition.FFL.FirstOrder.BinderNotation.«firstOrderFormula∀¹[_]_» : Lean.ParserDescr

The «first order formula∀¹[ ] » construction in FFL.FirstOrder.BinderNotation.

Equations

• One or more equations did not get rendered due to their size.

def PointwiseComposition.FFL.FirstOrder.BinderNotation.«firstOrderFormula∃¹[_]_» : Lean.ParserDescr

The «first order formula∃¹[ ] » construction in FFL.FirstOrder.BinderNotation.

Equations

• One or more equations did not get rendered due to their size.

def PointwiseComposition.FFL.FirstOrder.BinderNotation.«term“_|_”» : Lean.ParserDescr

The «term“ | ”» construction in FFL.FirstOrder.BinderNotation.

Equations

• One or more equations did not get rendered due to their size.

def PointwiseComposition.FFL.FirstOrder.BinderNotation.«term“_._”» : Lean.ParserDescr

The ”» construction in FFL.FirstOrder.BinderNotation.«term“_.

Equations

• One or more equations did not get rendered due to their size.

def PointwiseComposition.FFL.FirstOrder.BinderNotation.«term“_”» : Lean.ParserDescr

The «term“ ”» construction in FFL.FirstOrder.BinderNotation.

Equations

• One or more equations did not get rendered due to their size.

def PointwiseComposition.FFL.FirstOrder.BinderNotation.«firstOrderFormula_=_» : Lean.ParserDescr

The «first order formula = » construction in FFL.FirstOrder.BinderNotation.

Equations

• One or more equations did not get rendered due to their size.

def PointwiseComposition.FFL.FirstOrder.BinderNotation.«firstOrderFormula_<_» : Lean.ParserDescr

The «first order formula < » construction in FFL.FirstOrder.BinderNotation.

Equations

• One or more equations did not get rendered due to their size.

def PointwiseComposition.FFL.FirstOrder.BinderNotation.«firstOrderFormula_>_» : Lean.ParserDescr

The «first order formula > » construction in FFL.FirstOrder.BinderNotation.

Equations

• One or more equations did not get rendered due to their size.

def PointwiseComposition.FFL.FirstOrder.BinderNotation.«firstOrderFormula_≤_» : Lean.ParserDescr

The «first order formula ≤ » construction in FFL.FirstOrder.BinderNotation.

Equations

• One or more equations did not get rendered due to their size.

def PointwiseComposition.FFL.FirstOrder.BinderNotation.«firstOrderFormula_≥_» : Lean.ParserDescr

The «first order formula ≥ » construction in FFL.FirstOrder.BinderNotation.

Equations

• One or more equations did not get rendered due to their size.

def PointwiseComposition.FFL.FirstOrder.BinderNotation.«firstOrderFormula_∈_» : Lean.ParserDescr

The «first order formula ∈ » construction in FFL.FirstOrder.BinderNotation.

Equations

• One or more equations did not get rendered due to their size.

def PointwiseComposition.FFL.FirstOrder.BinderNotation.«firstOrderFormula_∋_» : Lean.ParserDescr

The «first order formula ∋ » construction in FFL.FirstOrder.BinderNotation.

Equations

• One or more equations did not get rendered due to their size.

def PointwiseComposition.FFL.FirstOrder.BinderNotation.«firstOrderFormula_≠_» : Lean.ParserDescr

The «first order formula ≠ » construction in FFL.FirstOrder.BinderNotation.

Equations

• One or more equations did not get rendered due to their size.

def PointwiseComposition.FFL.FirstOrder.BinderNotation.«firstOrderFormula_≮_» : Lean.ParserDescr

The «first order formula ≮ » construction in FFL.FirstOrder.BinderNotation.

Equations

• One or more equations did not get rendered due to their size.

def PointwiseComposition.FFL.FirstOrder.BinderNotation.«firstOrderFormula_≰_» : Lean.ParserDescr

The «first order formula ≰ » construction in FFL.FirstOrder.BinderNotation.

Equations

• One or more equations did not get rendered due to their size.

def PointwiseComposition.FFL.FirstOrder.BinderNotation.«firstOrderFormula_∉_» : Lean.ParserDescr

The «first order formula ∉ » construction in FFL.FirstOrder.BinderNotation.

Equations

• One or more equations did not get rendered due to their size.

def PointwiseComposition.FFL.FirstOrder.BinderNotation.«firstOrderFormula∀_<_,_» : Lean.ParserDescr

The «first order formula∀ < , » construction in FFL.FirstOrder.BinderNotation.

Equations

• One or more equations did not get rendered due to their size.

def PointwiseComposition.FFL.FirstOrder.BinderNotation.«firstOrderFormula∀_≤_,_» : Lean.ParserDescr

The «first order formula∀ ≤ , » construction in FFL.FirstOrder.BinderNotation.

Equations

• One or more equations did not get rendered due to their size.

def PointwiseComposition.FFL.FirstOrder.BinderNotation.«firstOrderFormula∀_∈_,_» : Lean.ParserDescr

The «first order formula∀ ∈ , » construction in FFL.FirstOrder.BinderNotation.

Equations

• One or more equations did not get rendered due to their size.

def PointwiseComposition.FFL.FirstOrder.BinderNotation.«firstOrderFormula∃_<_,_» : Lean.ParserDescr

The «first order formula∃ < , » construction in FFL.FirstOrder.BinderNotation.

Equations

• One or more equations did not get rendered due to their size.

def PointwiseComposition.FFL.FirstOrder.BinderNotation.«firstOrderFormula∃_≤_,_» : Lean.ParserDescr

The «first order formula∃ ≤ , » construction in FFL.FirstOrder.BinderNotation.

Equations

• One or more equations did not get rendered due to their size.

def PointwiseComposition.FFL.FirstOrder.BinderNotation.«firstOrderFormula∃_∈_,_» : Lean.ParserDescr

The «first order formula∃ ∈ , » construction in FFL.FirstOrder.BinderNotation.

Equations

• One or more equations did not get rendered due to their size.

def PointwiseComposition.FFL.FirstOrder.BinderNotation.unexpanderEq : Lean.PrettyPrinter.Unexpander

The unexpander Eq construction in FFL.FirstOrder.BinderNotation.

Equations

• One or more equations did not get rendered due to their size.

def PointwiseComposition.FFL.FirstOrder.BinderNotation.unexpanderLe : Lean.PrettyPrinter.Unexpander

The unexpander Le construction in FFL.FirstOrder.BinderNotation.

Equations

• One or more equations did not get rendered due to their size.

def PointwiseComposition.FFL.FirstOrder.BinderNotation.unexpandAnd : Lean.PrettyPrinter.Unexpander

The unexpand And construction in FFL.FirstOrder.BinderNotation.

Equations

• One or more equations did not get rendered due to their size.

def PointwiseComposition.FFL.FirstOrder.BinderNotation.unexpandOr : Lean.PrettyPrinter.Unexpander

The unexpand Or construction in FFL.FirstOrder.BinderNotation.

Equations

• One or more equations did not get rendered due to their size.

def PointwiseComposition.FFL.FirstOrder.BinderNotation.unexpandNeg : Lean.PrettyPrinter.Unexpander

The unexpand Neg construction in FFL.FirstOrder.BinderNotation.

Equations

• One or more equations did not get rendered due to their size.

def PointwiseComposition.FFL.FirstOrder.BinderNotation.unexpandUniv : Lean.PrettyPrinter.Unexpander

The unexpand Univ construction in FFL.FirstOrder.BinderNotation.

Equations

• One or more equations did not get rendered due to their size.

def PointwiseComposition.FFL.FirstOrder.BinderNotation.unexpandEx : Lean.PrettyPrinter.Unexpander

The unexpand Ex construction in FFL.FirstOrder.BinderNotation.

Equations

• One or more equations did not get rendered due to their size.

def PointwiseComposition.FFL.FirstOrder.BinderNotation.unexpandBall : Lean.PrettyPrinter.Unexpander

The unexpand Ball construction in FFL.FirstOrder.BinderNotation.

Equations

• One or more equations did not get rendered due to their size.

def PointwiseComposition.FFL.FirstOrder.BinderNotation.unexpandBex : Lean.PrettyPrinter.Unexpander

The unexpand Bex construction in FFL.FirstOrder.BinderNotation.

Equations

• One or more equations did not get rendered due to their size.

def PointwiseComposition.FFL.FirstOrder.BinderNotation.unexpandArrow : Lean.PrettyPrinter.Unexpander

The unexpand Arrow construction in FFL.FirstOrder.BinderNotation.

Equations

• One or more equations did not get rendered due to their size.

def PointwiseComposition.FFL.FirstOrder.BinderNotation.unexpandIff : Lean.PrettyPrinter.Unexpander

The unexpand Iff construction in FFL.FirstOrder.BinderNotation.

Equations

• One or more equations did not get rendered due to their size.

def PointwiseComposition.FFL.FirstOrder.BinderNotation.unexpandOpArith : Lean.PrettyPrinter.Unexpander

The unexpand Op Arith construction in FFL.FirstOrder.BinderNotation.

Equations

• One or more equations did not get rendered due to their size.

Notation for formula as term

def PointwiseComposition.FFL.FirstOrder.BinderNotation.«termF‘_’» : Lean.ParserDescr

The «term F‘ ’» construction in FFL.FirstOrder.BinderNotation.

Equations

• One or more equations did not get rendered due to their size.

def PointwiseComposition.FFL.FirstOrder.BinderNotation.«termF‘_|_’» : Lean.ParserDescr

The «term F‘ | ’» construction in FFL.FirstOrder.BinderNotation.

Equations

• One or more equations did not get rendered due to their size.

def PointwiseComposition.FFL.FirstOrder.BinderNotation.«termF‘_._’» : Lean.ParserDescr

The ’» construction in FFL.FirstOrder.BinderNotation.«termF‘_.

Equations

• One or more equations did not get rendered due to their size.

def PointwiseComposition.FFL.FirstOrder.BinderNotation.«termF“_|_”» : Lean.ParserDescr

The «term F“ | ”» construction in FFL.FirstOrder.BinderNotation.

Equations

• One or more equations did not get rendered due to their size.

def PointwiseComposition.FFL.FirstOrder.BinderNotation.«termF“_._”» : Lean.ParserDescr

The ”» construction in FFL.FirstOrder.BinderNotation.«termF“_.

Equations

• One or more equations did not get rendered due to their size.

def PointwiseComposition.FFL.FirstOrder.BinderNotation.«termF“_”» : Lean.ParserDescr

The «term F“ ”» construction in FFL.FirstOrder.BinderNotation.

Equations

• One or more equations did not get rendered due to their size.