2019-12-10から1日間の記事一覧
TopProver 問37 Zero test https://top-prover.top/problem/37 Inductive iszero : nat -> Prop := | iszero_0 : iszero 0 | iszero_S : forall n, iszero (S n) -> iszero n. Definition task := forall n, iszero n <-> n = 0. まだcoqに慣れないので翻訳…
TopProver 問37 Zero test https://top-prover.top/problem/37 Inductive iszero : nat -> Prop := | iszero_0 : iszero 0 | iszero_S : forall n, iszero (S n) -> iszero n. Definition task := forall n, iszero n <-> n = 0. まだcoqに慣れないので翻訳…