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