righ1113

module Isort

-- > idris -p base
import Syntax.PreorderReasoning

%default total
%hide sorted


sorted : List Nat -> Bool

righ1113

module CoInductive

%default total


-- 性質Q
codata Q : Stream Nat -> Type where
  Qcons : (x:Nat) -> Q xs -> Q (x::xs)

isQ : (xs:Stream Nat) -> Q xs

righ1113

judge finite unfoldr by Idris

unfoldrが有限項か判定したい

原理的に無理なのか

/libs/contrib/Data/CoList.idr
でCoListとunfoldrは以下のように実装されている。

righ1113

open list (hiding reverse)

#check 1
#reduce head [0, 1, 2, 3]


variable {T : Type}

def snoc : list T → T → list T

righ1113

open nat
#check succ


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

righ1113

module MultiOf3

%default total


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

-- 3の倍数か判定する

righ1113

module CosineFormula

-- > idris -p base
import Syntax.PreorderReasoning

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

righ1113

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


--
-- Codes

righ1113

module MagicSquare where

import Data.List (permutations)


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

righ1113

module EightPuzzle where

import Data.List (permutations)


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