Compiler.NaturalOperation

32def lookupNaturalOperation =
33  (lambda unrestricted input : Bytes .
34    (app
35      (nat-eliminate
36        (lambda unrestricted flag : Nat .
37          (pi unrestricted force : Nat . (family NaturalOperationLookup)))
38        (lambda unrestricted force : Nat .
39          (app
40            (nat-eliminate
41              (lambda unrestricted flag : Nat .
42                (pi unrestricted force : Nat . (family NaturalOperationLookup)))
43              (lambda unrestricted force : Nat .
44                (app
45                  (nat-eliminate
46                    (lambda unrestricted flag : Nat .
47                      (pi unrestricted force : Nat . (family NaturalOperationLookup)))
48                    (lambda unrestricted force : Nat .
49                      (app
50                        (nat-eliminate
51                          (lambda unrestricted flag : Nat .
52                            (pi unrestricted force : Nat . (family NaturalOperationLookup)))
53                          (lambda unrestricted force : Nat .
54                            (app
55                              (nat-eliminate
56                                (lambda unrestricted flag : Nat .
57                                  (pi unrestricted force : Nat . (family NaturalOperationLookup)))
58                                (lambda unrestricted force : Nat .
59                                  (constructor NaturalOperationLookup NaturalOperationMissing))
60                                (lambda unrestricted predecessor : Nat .
61                                  (lambda unrestricted induction : (pi unrestricted force : Nat . (family NaturalOperationLookup)) .
62                                    (lambda unrestricted force : Nat .
63                                      (constructor
64                                        NaturalOperationLookup
65                                        NaturalOperationFound
66                                        (constructor CoreNaturalOperation CoreNaturalModulo)))))
67                                (bytes-equal input b"nat-modulo"))
68                              zero))
69                          (lambda unrestricted predecessor : Nat .
70                            (lambda unrestricted induction : (pi unrestricted force : Nat . (family NaturalOperationLookup)) .
71                              (lambda unrestricted force : Nat .
72                                (constructor
73                                  NaturalOperationLookup
74                                  NaturalOperationFound
75                                  (constructor CoreNaturalOperation CoreNaturalDivide)))))
76                          (bytes-equal input b"nat-divide"))
77                        zero))
78                    (lambda unrestricted predecessor : Nat .
79                      (lambda unrestricted induction : (pi unrestricted force : Nat . (family NaturalOperationLookup)) .
80                        (lambda unrestricted force : Nat .
81                          (constructor
82                            NaturalOperationLookup
83                            NaturalOperationFound
84                            (constructor CoreNaturalOperation CoreNaturalMultiply)))))
85                    (bytes-equal input b"nat-multiply"))
86                  zero))
87              (lambda unrestricted predecessor : Nat .
88                (lambda unrestricted induction : (pi unrestricted force : Nat . (family NaturalOperationLookup)) .
89                  (lambda unrestricted force : Nat .
90                    (constructor
91                      NaturalOperationLookup
92                      NaturalOperationFound
93                      (constructor CoreNaturalOperation CoreNaturalSubtract)))))
94              (bytes-equal input b"nat-subtract"))
95            zero))
96        (lambda unrestricted predecessor : Nat .
97          (lambda unrestricted induction : (pi unrestricted force : Nat . (family NaturalOperationLookup)) .
98            (lambda unrestricted force : Nat .
99              (constructor
100                NaturalOperationLookup
101                NaturalOperationFound
102                (constructor CoreNaturalOperation CoreNaturalAdd)))))
103        (bytes-equal input b"nat-add"))
104      zero))