Open ryuta-ito opened 4 years ago
Inductive prop : Type := | atomp (n : nat) : prop (* P_1 P_2, ... *) | notp (p : prop) : prop | andp (p q : prop) : prop | orp (p q : prop) : prop | impp (p q : prop) : prop.
のようなケースがうまく動かない
Notation "[ x ; .. ; y ]" := (cons x .. (cons y nil) ..).
のようなケースも動かない
のようなケースがうまく動かない