diff --git a/website/docs/reference/functions.md b/website/docs/reference/functions.md index 71e8ddd5a..576df882d 100644 --- a/website/docs/reference/functions.md +++ b/website/docs/reference/functions.md @@ -25,14 +25,14 @@ S32 -> S32 -> S32 Function types are also types: -``` +```pikelet U32 -> U32 : Type ``` In order to find the universe level of a function type, we use the universe level the largest input or output: -``` +```pikelet U32 -> Type^2 : Type^3 ``` diff --git a/website/docs/reference/records.md b/website/docs/reference/records.md index 9ffd0d3d7..3c63f922f 100644 --- a/website/docs/reference/records.md +++ b/website/docs/reference/records.md @@ -41,7 +41,7 @@ Here the type of `a` _depends_ on the type given to `A`. Record types are also types: -``` +```pikelet Record { first : U32, } : Type