原始帰納的函数; prf 原始帰納的函数(primitive recursive function; prf)とは, 以下で定義される函数 $ \mathbb{N}^n \to \mathbb{N} $ のこと: 定数函数 $zero : \mathbb{N}^0 \to \mathbb{N}$, 後続函数 $suc : \mathbb{N} \to \mathbb{N}$, 射影函数 $p^…

概要 RPGの戦闘システムとして考えたやつ。戦闘は普通のターン制。各ターンに1つのアクションが取れる(攻撃・防御・回復 など)。 プレイヤーは戦闘の前に、アクションを並べて作った列をスロットという形で保存しておく。 敵との戦闘時、プレイヤーの作った…

Haskellで型レベルプログラミング(あるいはごく簡単な証明)を書くときに, DataKindsでデータ型をそのまま持ち上げると困る場面がある. {-# LANGUAGE DataKinds, GADTs, TypeOperators, TypeFamilies #-} data a :=: b where Refl :: a :=: a data Nat = Zero…