我想拿一个字符串然后变成一个列表Direction.例如,"UDDUD"应该返回[U,D,D,U,D],而任何不包含U或D返回的字符串Nothing(例如"UDYD"返回Nothing).
data Direction = U | D
deriving (Show, Eq)
-- where U is Up and D is Down
findDirection :: [Char] -> Maybe [Direction]
findDirection [] = Nothing
findDirection ['U'] = Just [U]
findDirection ['D'] = Just [D]
findDirection (x:xs)
| x == 'U' = Just (U : findDirection xs)
| x == 'D' = Just (D : findDirection xs)
| otherwise = Nothing
我收到以下错误: …
如果其中一个是偶数而另一个是奇数,则采用"两个自然之和很奇怪"的非常简单的证明:
Require Import Arith.
Require Import Coq.omega.Omega.
Definition even (n: nat) := exists k, n = 2 * k.
Definition odd (n: nat) := exists k, n = 2 * k + 1.
Lemma sum_odd_even : forall n m, odd (n + m) -> odd n /\ even m \/ even n /\ odd m.
Proof.
intros n. intros m. left.
destruct H. firstorder.
这段代码末尾的状态是:
2 subgoals
n, m, x : nat
H : n + m = 2 * …