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

-- 参考記事：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

{-
参考記事：
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

module Godel07

%default total
%hide Functor


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

righ1113

;; > egison -N
;; > loadFile("multiOf3-N.egi")


def sumMulti?(x, n2, y) =
  match (sum(map(($i -> x_i), 1..n2)) + y) as mod(3)
    | 0 -> #t
    | _ -> #f

def afterCheck?(ans) =

righ1113

;; > egison -N
;; > loadFile("poker-N.egi")

;;;
;;;
;;; Poker-hands demonstration
;;;
;;;

;;

righ1113

;; > egison -N
;; > loadFile("sudoku-N.egi")


def parse(str) = map(read, map(1#pack([%1]),
  match S.replace(".", "0", str) as string
  | loop($i, (1, 81, _), <cons $x_i ...>, <nil>) -> map(($i -> x_i), 1..81) ))

;; checkHintPattern
def chp(n, str) = let hintValue = nth(n, parse(str)) in

righ1113

// main.rsにコピペする

// Cargo.toml
// [dependencies]
// num-traits = "0.2.7"
// num-bigint = "0.2"


extern crate num_traits;
extern crate num_bigint;

righ1113

★★★19/10/27　理解できた
★★★19/10/22　理解できなかった
cpl> simp add1.pair(o, s.s.o)
0:add1.pair(o,s.s.o)*I
1[1]:pair(o,s.s.o)*I
2:add1*pair(o,s.s.o)
  let add1 = ev.prod(pr(cur(pi2), cur(s.ev)),     nat);   add1が
  let add3 = ev.pair(pr(cur(pi2), cur(s.ev)).pi1, pi2);   add3と同じになってる
3:ev.pair(pr(cur(pi2),cur(s.ev)).pi1,pi2)*pair(o,s.s.o)
4[1]:pair(pr(cur(pi2),cur(s.ev)).pi1,pi2)*pair(o,s.s.o)

righ1113

/*
  https://github.com/bmstu-iu9/refal-5-lambda

  > chcp 65001
  > srefc.bat test01.ref
*/

/* 先頭と末尾が同じ文字なら、それを削っていく */
Pal {
              = True;