righ1113

module Godel07

%default total
%hide Functor


-- 証明をYesコンストラクタでくるんで、Proofable型にする
data Proofable : Type -> Type where
  Yes : (prf : prop) -> Proofable prop

righ1113

{-
参考記事：
https://qiita.com/Lugendre/items/6b4a8c8a9c85fcdcb292
https://qiita.com/waddlaw/items/49874f4cf9b680e4b015
-}
{-# LANGUAGE Arrows #-}
module ArrowExample where

import Prelude hiding (id, (.))
import Control.Category (Category(..))

righ1113

-- 参考記事：https://mkotha.hatenadiary.org/entry/20110430/1304122048
module BreakLoop where

import Prelude hiding (take)


myLoop :: (accT -> a -> (accT -> b) -> b) -> (accT -> b) -> accT -> [a] -> b
myLoop _ g acc []     = g acc
myLoop f g acc (x:xs) = f acc x $ \acc' -> myLoop f g acc' xs

righ1113

-- module Ramsey05
module Main

%default total


comb : Nat -> List a -> List (List a)
comb Z     _         = [[]]
comb (S n) []        = []
comb (S n) (x :: xs) = [x :: y | y <- comb n xs] ++ comb (S n) xs

righ1113

module EightPuzzle where

import Data.List (permutations)


-- 参考記事：https://mathtrain.jp/8puzzle
{--
    8 puzzle
    1 2 3

righ1113

module MagicSquare where

import Data.List (permutations)


{--
    3*3 Magic square
    a b c
    d e f

righ1113

--
-- zundoko kiyoshi
--
-- $ egison                                       4.1.3
-- > loadFile "zdk.egi"
-- > zdk


--
-- Codes

righ1113

module CosineFormula

-- > idris -p base
import Syntax.PreorderReasoning

%default total
%hide Language.Reflection.P
%hide cos

righ1113

module MultiOf3

%default total


-- isMm3 y x : -3y + x
data Mm3 : (y : Nat) -> Type where
  isMm3 : (y : Nat) -> Nat -> Mm3 y

-- 3の倍数か判定する

righ1113

open nat
#check succ


-- isMm3 y x : -3y + x
inductive Mm3 (y : ℕ)
| isMm3 : ℕ → Mm3
open Mm3
#check isMm3 3 5