Print eq. (* ===> Inductive eq (A : Type) (x : A) : A -> Prop := eq_refl : x = x *)eq_reflは引数を持たないコンストラクタ。 eq_reflを実行すると、なんらかの型Aの値xを取って、 eq x x (x = x)という命題型の値(つまり証明or根拠)を返す関数？を返す…

式の変形その1 Reserved Notation "e '==>' e'" (at level 50, left associativity). Inductive ReduceNatExpR : Exp -> Exp -> Prop := | R_Plus : forall n1 n2 n3, n1 plus n2 is n3 -> (ExpConst n1) +_ (ExpConst n2) ==> ExpConst n3 | R_Times : fora…

式の定義 Inductive Exp : Type := | ExpConst : nat -> Exp | ExpPlus : Exp -> Exp -> Exp | ExpMult : Exp -> Exp -> Exp. Notation "x '+_' y" := (ExpPlus x y) (at level 50): type_scope. Notation "x '*_' y" := (ExpMult x y) (at level 40): type_…

なんか読書会がもうすぐあって結構な人気らしい。行って覗いてみたい気もするが、すでに定員一杯らしいし、Haskell知らんし、そもそも勉強会読書会なるものについてける気もしないしちょっと無理だろう。件の本は、オンライン演習は一通りやったけど、そうい…

懲りずにソフトウェアの基礎を読み返してるけど、Imp.vあたりから急に難しくなるのはやっぱり気のせいではないと思う。いや、まあそれまでも分からんところはまだ分からんけど。鳩の巣とか回文とか。型付ラムダ計算あたりまでは何とか読みたいところではある…