@@ -97,6 +97,7 @@ applyDataOptRT n tag arity uniq args
98 -- Nat special cases
98 -- Nat special cases
99 -- TODO: Would be nice if this was configurable in idris source!
99 -- TODO: Would be nice if this was configurable in idris source!
100+ -- Issue #1597 https://github.com/idris-lang/Idris-dev/issues/1597
100 doOpts (NS (UN z) [nat, prelude]) []
101 doOpts (NS (UN z) [nat, prelude]) []
101 | z == txt "Z" && nat == txt "Nat" && prelude == txt "Prelude"
102 | z == txt "Z" && nat == txt "Nat" && prelude == txt "Prelude"
102 = Constant (BI 0)
103 = Constant (BI 0)
@@ -105,4 +106,3 @@ applyDataOptRT n tag arity uniq args
105 = App (App (P Ref (sUN "prim__addBigInt") Erased) k) (Constant (BI 1))
106 = App (App (P Ref (sUN "prim__addBigInt") Erased) k) (Constant (BI 1))
107 doOpts n args = mkApp (P (DCon tag arity uniq) n Erased) args
108 doOpts n args = mkApp (P (DCon tag arity uniq) n Erased) args