@@ -339,9 +339,8 @@ this means the rule applies to (object) variables declared to have type
|
|||||||
our system. A single rule takes care of figuring the types of _all_
|
our system. A single rule takes care of figuring the types of _all_
|
||||||
variables.
|
variables.
|
||||||
|
|
||||||
{{< todo >}}
|
> [!TODO]
|
||||||
The rest of this, but mostly statements.
|
> The rest of this, but mostly statements.
|
||||||
{{< /todo >}}
|
|
||||||
|
|
||||||
### This Page at a Glance
|
### This Page at a Glance
|
||||||
#### Metavariables
|
#### Metavariables
|
||||||
|
|||||||
@@ -17,7 +17,8 @@ spend time explaining dependent types, nor the syntax for them in Idris,
|
|||||||
which is the language I'll use in this article. Below are a few resources
|
which is the language I'll use in this article. Below are a few resources
|
||||||
that should help you get up to speed.
|
that should help you get up to speed.
|
||||||
|
|
||||||
{{< todo >}}List resources{{< /todo >}}
|
> [!TODO]
|
||||||
|
> List resources
|
||||||
|
|
||||||
We've seen that, given a function `F a -> a`, we can define a function
|
We've seen that, given a function `F a -> a`, we can define a function
|
||||||
`B -> a`, if `F` is a base functor of the type `B`. However, what if
|
`B -> a`, if `F` is a base functor of the type `B`. However, what if
|
||||||
|
|||||||
Submodule themes/vanilla updated: 4ff04221b0...806d3a318f
Reference in New Issue
Block a user