We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
1 parent f89e9f3 commit 28ce4caCopy full SHA for 28ce4ca
1 file changed
Prelude.tel
@@ -67,10 +67,13 @@ dEqual = \a b -> let equalsOne = \x -> if x then (not (left x)) else 0
67
in if a then equalsOne (d2c (left a) (\x -> left x) b)
68
else not b
69
70
-dDiv = \a b -> { \p -> dMinus (left p) (right p)
71
- , \recur p -> succ (recur (dMinus (left p) (right p), right p))
72
- , \p -> if (dEqual (left p) (right p)) then succ 0 else 0
73
- } (a, b)
+dDiv = \a b -> if (dEqual b 0)
+ then abort "Undefined"
+ else
+ { \p -> dMinus (left p) (right p)
74
+ , \recur p -> succ (recur (dMinus (left p) (right p), right p))
75
+ , \p -> if (dEqual (left p) (right p)) then succ 0 else 0
76
+ } (a, b)
77
78
listLength = foldr (\a b -> succ b) 0
79
0 commit comments