diff --git a/DocGen4/Output/FoundationalTypes.lean b/DocGen4/Output/FoundationalTypes.lean index b1e00a7..7ece5c7 100644 --- a/DocGen4/Output/FoundationalTypes.lean +++ b/DocGen4/Output/FoundationalTypes.lean @@ -34,17 +34,19 @@ def foundationalTypes : BaseHtmlM Html := templateLiftExtends (baseHtml "Foundat
Note that these can also be written with the alternative notations:
∀ a : α, β a
, conventionally used where β a : Prop
.(a : α) → β a
α → γ
, possible only if β a = γ
for all a
.Lean also permits ASCII-only spellings of the three variants:
Pi a : A, B a
for {"Π a : α, β a"}
forall a : A, B a
for {"∀ a : α, β a"}
(a : A) -> B a
, for (a : α) → β a
A -> B
, for α → β
Note that despite not itself being a function, (→)
is available as infix notation for
{"λ α β, α → β"}
.