Compiler.NaturalOperation

106def decodeNaturalOperation =
107  (lambda unrestricted input : Byte .
108    (app
109      (nat-eliminate
110        (lambda unrestricted flag : Nat .
111          (pi unrestricted force : Nat . (family NaturalOperationLookup)))
112        (lambda unrestricted force : Nat .
113          (app
114            (nat-eliminate
115              (lambda unrestricted flag : Nat .
116                (pi unrestricted force : Nat . (family NaturalOperationLookup)))
117              (lambda unrestricted force : Nat .
118                (app
119                  (nat-eliminate
120                    (lambda unrestricted flag : Nat .
121                      (pi unrestricted force : Nat . (family NaturalOperationLookup)))
122                    (lambda unrestricted force : Nat .
123                      (app
124                        (nat-eliminate
125                          (lambda unrestricted flag : Nat .
126                            (pi unrestricted force : Nat . (family NaturalOperationLookup)))
127                          (lambda unrestricted force : Nat .
128                            (app
129                              (nat-eliminate
130                                (lambda unrestricted flag : Nat .
131                                  (pi unrestricted force : Nat . (family NaturalOperationLookup)))
132                                (lambda unrestricted force : Nat .
133                                  (constructor NaturalOperationLookup NaturalOperationMissing))
134                                (lambda unrestricted predecessor : Nat .
135                                  (lambda unrestricted induction : (pi unrestricted force : Nat . (family NaturalOperationLookup)) .
136                                    (lambda unrestricted force : Nat .
137                                      (constructor
138                                        NaturalOperationLookup
139                                        NaturalOperationFound
140                                        (constructor CoreNaturalOperation CoreNaturalModulo)))))
141                                (byte-equal input (byte 4)))
142                              zero))
143                          (lambda unrestricted predecessor : Nat .
144                            (lambda unrestricted induction : (pi unrestricted force : Nat . (family NaturalOperationLookup)) .
145                              (lambda unrestricted force : Nat .
146                                (constructor
147                                  NaturalOperationLookup
148                                  NaturalOperationFound
149                                  (constructor CoreNaturalOperation CoreNaturalDivide)))))
150                          (byte-equal input (byte 3)))
151                        zero))
152                    (lambda unrestricted predecessor : Nat .
153                      (lambda unrestricted induction : (pi unrestricted force : Nat . (family NaturalOperationLookup)) .
154                        (lambda unrestricted force : Nat .
155                          (constructor
156                            NaturalOperationLookup
157                            NaturalOperationFound
158                            (constructor CoreNaturalOperation CoreNaturalMultiply)))))
159                    (byte-equal input (byte 2)))
160                  zero))
161              (lambda unrestricted predecessor : Nat .
162                (lambda unrestricted induction : (pi unrestricted force : Nat . (family NaturalOperationLookup)) .
163                  (lambda unrestricted force : Nat .
164                    (constructor
165                      NaturalOperationLookup
166                      NaturalOperationFound
167                      (constructor CoreNaturalOperation CoreNaturalSubtract)))))
168              (byte-equal input (byte 1)))
169            zero))
170        (lambda unrestricted predecessor : Nat .
171          (lambda unrestricted induction : (pi unrestricted force : Nat . (family NaturalOperationLookup)) .
172            (lambda unrestricted force : Nat .
173              (constructor
174                NaturalOperationLookup
175                NaturalOperationFound
176                (constructor CoreNaturalOperation CoreNaturalAdd)))))
177        (byte-equal input (byte 0)))
178      zero))