a-conjecture-of-mine

An exercise on polyglossy: the same problem solved on multiple languages

git clone: git://git.pablopie.xyz/a-conjecture-of-mine
Log
Files
Refs

Commit: 4caf6d369930d63947b45544ca9a9bb090f5fd9a
Parent: ff512183d5897c369c0366bb77e4077a0db0057e
Author: Pablo Escobar Gaviria <gark.garcia@protonmail.com>
Date: Sat, 15 Feb 2020 08:53:15 -0200

Fixed errors in the Idris implementation.

Diffstat

1 file changed, 2 insertions, 21 deletions

Status	File Name	N° Changes	Insertions	Deletions
Modified	Idris/Main.idr	23	2	21

diff --git a/Idris/Main.idr b/Idris/Main.idr
@@ -5,8 +5,6 @@
 
 module Main
 
-import System
-
 data Every : (Nat -> Type) -> Nat -> Type  where
     Base :  {P : Nat -> Type} -> Every P Z
     Succ :  (n : Nat)
@@ -15,37 +13,20 @@ data Every : (Nat -> Type) -> Nat -> Type  where
          -> P (S n) 
          -> Every P (S n)
 
-head' : List a -> Maybe a
-head' [] = Nothing
-head' (x :: _) = Just x
-
-readDec : String -> List (Nat, String)
-readDec = ?readDec
-
-main : IO Int
-main = do
-    args <- getArgs
-        
-    case readDec <$> head' args of
-        Just [(max, "")] =>
-            if counter' max then exitFailure else exitSuccess
-        _ => 
-            exitInvalidInput
-
 -- Calculates the sum of the digits of `n`.
 sumDigits : Nat -> Int
 sumDigits = sumDigitsTail 0
     where
         sumDigitsTail : Int -> Nat -> Int
         sumDigitsTail acc Z = acc
-        sumDegitsTail acc n = sumDigitsTail (acc + fromEnum n `mod` 10) 
+        sumDigitsTail acc n = sumDigitsTail (acc + fromNat n `mod` 10) 
                                             (n `div` 10)
 
 diff : Nat -> Nat -> Int
 diff a b = (sumDigits (a + b) - sumDigits a - sumDigits b) `mod` 9
 
 -- TODO: Prove this
-test : Nat -> Nat -> diff a b = 0
+test : (a : Nat) -> (b : Nat) -> diff a b = 0
 test = ?test
 
 iter : (a : Nat) -> Every (test a) a