righ1113

righ1113

-- Egison Version >= 3.10.0
-- $ egison -N
-- > loadFile "prover1.egins"



--
-- Matcher
--

righ1113

***(
  > load test02.maude
)

fmod NAT is
  sorts Zero NzNat Nat .
  subsort Zero NzNat < Nat .

  op o   :         -> Zero  [ctor] .
  op s_  : Nat     -> NzNat [ctor] .

righ1113

-- > Egison Version == 3.9.4
-- > egison -N
-- > loadFile "rewriteNat1.egins"



--
-- Utils
--

righ1113

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

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

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

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

// main.rsにコピペする

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


extern crate num_traits;
extern crate num_bigint;

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

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

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

;;

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) =