@@ -86,33 +86,38 @@ This code generates the following data and function:
87.. code-block:: idris
87.. code-block:: idris
89−data U : Type where
89+ data U : Type where
91− Pi : (code : U) -> (el code -> U) -> U
91+ Pi : (code : U) -> (el code -> U) -> U
92− el : U -> Type
92+ el : U -> Type
93− el (Pi code body) = (x : el code) -> el (body x)
93+ el (Pi code body) = (x : el code) -> el (body x)
94− el Base = Bool
94+ el Base = Bool
96−Which can be used like this:
96+.. list-table:: Usage
98+ * - We can then use U the data structure, like this:
98−.. code-block:: idris
101+ .. code-block:: idris
100− λΠ> :t U
103+ λΠ> :t U
101− U : Type
104+ U : Type
102− λΠ> :doc U
105+ λΠ> :doc U
103− No documentation for U
106+ No documentation for U
104− λΠ> Base
107+ λΠ> Base
105− Base : U
108+ Base : U
106− λΠ> DataDef.Pi
109+ λΠ> DataDef.Pi
107− Pi : (code : U) -> (el code -> U) -> U
110+ Pi : (code : U) -> (el code -> U) -> U
112+ * - el is the function that has been defined:
110−.. code-block:: idris
115+ .. code-block:: idris
112− λΠ> :t el
117+ λΠ> :t el
113− el : U -> Type
118+ el : U -> Type
114− λΠ> el Base
119+ λΠ> el Base
115− Bool : Type
120+ Bool : Type
117So these are the functions that we can use to create data and functions in the Elab monad:
122So these are the functions that we can use to create data and functions in the Elab monad: