pe200012

;; Macro to define algebraic data types
;; Usage:
;; (defdata Maybe
;;   Nothing              ; Nullary constructor (no arguments)
;;   [Just val]          ; N-ary constructor with positional fields
;;   (Good a b c))       ; Record constructor with named fields
;;
;; This will create a local table `Maybe` with constructors:
;; Maybe.Nothing()                    ; Returns {:variant "Nothing"}
;; Maybe.Just(val)                    ; Returns {:variant "Just" :fields [val]}

pe200012

Haskell    54 mins        ████████████████████▏  96.0%
Text       2 mins         ▊░░░░░░░░░░░░░░░░░░░░   4.0%

pe200012

open import Level                                      using (_⊔_)
open import Function                                   using (_∘_)
open import Data.Vec                                   using (Vec; []; _∷_; foldr)
open import Data.Nat                                   using (ℕ; zero; suc; _+_)
open import Data.Nat.Properties.Simple                 using (+-right-identity; +-suc)
open import Data.Sum                                   using (_⊎_; inj₁; inj₂)
open import Data.Product                               using (∃; _×_; _,_; proj₁; proj₂)
open import Data.Empty                                 using (⊥-elim)
open import Relation.Nullary                           using (Dec; yes; no; ¬_)
open import Relation.Binary                            using (module DecTotalOrder; DecTotalOrder; Rel)

pe200012

module Lib where
-- 4


-- >>> euler 10

-- | euler's totient function
--
-- euler's totient function is defined as the number of positive integers
-- less than or equal to n which are coprime to n.

pe200012

{-# LANGUAGE ViewPatterns #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE DeriveFoldable #-}
{-# LANGUAGE DeriveTraversable #-}