unfoldrが有限項か判定したい
/libs/contrib/Data/CoList.idr
でCoList
とunfoldr
は以下のように実装されている。
module Isort | |
-- > idris -p base | |
import Syntax.PreorderReasoning | |
%default total | |
%hide sorted | |
sorted : List Nat -> Bool |
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 |
open list (hiding reverse) | |
#check 1 | |
#reduce head [0, 1, 2, 3] | |
variable {T : Type} | |
def snoc : list T → T → list T |
open nat | |
#check succ | |
-- isMm3 y x : -3y + x | |
inductive Mm3 (y : ℕ) | |
| isMm3 : ℕ → Mm3 | |
open Mm3 | |
#check isMm3 3 5 |
module MultiOf3 | |
%default total | |
-- isMm3 y x : -3y + x | |
data Mm3 : (y : Nat) -> Type where | |
isMm3 : (y : Nat) -> Nat -> Mm3 y | |
-- 3の倍数か判定する |
module CosineFormula | |
-- > idris -p base | |
import Syntax.PreorderReasoning | |
%default total | |
%hide Language.Reflection.P | |
%hide cos | |
-- | |
-- zundoko kiyoshi | |
-- | |
-- $ egison 4.1.3 | |
-- > loadFile "zdk.egi" | |
-- > zdk | |
-- | |
-- Codes |
module MagicSquare where | |
import Data.List (permutations) | |
{-- | |
3*3 Magic square | |
a b c | |
d e f |
module EightPuzzle where | |
import Data.List (permutations) | |
-- 参考記事:https://mathtrain.jp/8puzzle | |
{-- | |
8 puzzle | |
1 2 3 |