diff --git a/DocGen4/Output/FoundationalTypes.lean b/DocGen4/Output/FoundationalTypes.lean index 8c8217e5..3eb694e2 100644 --- a/DocGen4/Output/FoundationalTypes.lean +++ b/DocGen4/Output/FoundationalTypes.lean @@ -40,12 +40,12 @@ def foundationalTypes : BaseHtmlM Html := templateLiftExtends (baseHtml "Foundat
Lean also permits ASCII-only spellings of the three variants:
forall a : A, B a
for {"∀ a : α, β a"}
(a : A) -> B a
, for (a : α) → β a
A -> B
, for α → β
{"(a : A) -> B a"}
, for (a : α) → β a
{"A -> B"}
, for α → β
Note that despite not itself being a function, (→)
is available as infix notation for
- {"fun α β, α → β"}
.
{"fun α β, α → β"}
.
+ -- TODO: instances for pi types
end DocGen4.Output