@@ -42,10 +42,12 @@ This was generated by the following code:
4242
4343 addTwo : Elab ()
4444 addTwo = do let twoname : TTName = `{{TwoDef.Two}}
45+ let F2 = `{{TwoDef.F}}
46+ let T2 = `{{TwoDef.T}}
4547 declareDatatype $ Declare twoname [] `(Type)
4648 defineDatatype $ DefineDatatype twoname [
47− Constructor `{{F}} [] (Var `{{TwoDef.Two}}),
48− Constructor `{{T}} [] (Var `{{TwoDef.Two}})
49+ Constructor `{{F}} [] (Var `{{TwoDef.Two}}),
50+ Constructor `{{T}} [] (Var `{{TwoDef.Two}})
4951 ]
5052
5153 %runElab addTwo
@@ -96,31 +98,29 @@ Note: The left hand side (lhs) and right hand side (rhs) of FunClause typically
9698
9799 λΠ> :printdef perm1
98100 perm1 : Two -> Two
99− F = F
100− T = T
101+ perm1 F = F
102+ perm1 T = T
101103 λΠ> :printdef perm2
102104 perm2 : Two -> Two
103− F = F
104− T = T
105+ perm1 F = T
106+ perm1 T = F
105107
106108This was generated with the following code:
107109
108110.. code-block:: idris
109111
110112 let perm1 = `{{TwoDef.perm1}}
111− let F2 = `{{TwoDef.F}}
112− let T2 = `{{TwoDef.T}}
113113 declareType (Declare perm1 [MkFunArg `{{code}} (Var twoname) Explicit NotErased] (Var twoname))
114114 defineFunction $ DefineFun perm1 [
115− MkFunClause (Var F2) (Var F2),
116− MkFunClause (Var T2) (Var T2)
115+ MkFunClause (RApp (Var perm1) (Var `{{TwoDef.F}})) (Var F2),
116+ MkFunClause (RApp (Var perm1) (Var `{{TwoDef.T}})) (Var T2)
117117 ]
118118
119119 let perm2 = `{{TwoDef.perm2}}
120120 declareType (Declare perm2 [MkFunArg `{{code}} (Var twoname) Explicit NotErased] (Var twoname))
121121 defineFunction $ DefineFun perm2 [
122− MkFunClause (Var F2) (Var T2),
123− MkFunClause (Var T2) (Var F2)
122+ MkFunClause (RApp (Var perm1) (Var `{{TwoDef.F}})) (Var T2),
123+ MkFunClause (RApp (Var perm1) (Var `{{TwoDef.T}})) (Var F2)
124124 ]
125125
126126.. list-table::
@@ -128,10 +128,14 @@ This was generated with the following code:
128128 * - This is what happens when we call the functions:
129129 - .. code-block:: idris
130130
131+ λΠ> perm1 F
132+ F : Two
131133 λΠ> perm1 T
132− F T : Two
134+ T : Two
135+ λΠ> perm2 F
136+ T : Two
133137 λΠ> perm2 T
134− F T : Two
138+ F : Two
135139
136140So far these datatypes and functions could have been written, statically, in the usual way. However, it is possible to imagine situations where we may need a lot of functions to be generated automatically at compile time. For example, if we extend this Boolean datatype to a datatype with more simple constructors (a finite set), we could generate a function for every possible permutation of that datatype back to itself.
137141