小编Ily*_*sov的帖子

我在玩归纳命题。我有以下归纳定义：

Inductive subseq {X : Type} : list X -> list X -> Prop :=
| empty_subseq : subseq [ ] [ ]
| subseq_left_elim : forall (l1 l2 : list X) (x : X),
              subseq (x :: l1) l2 -> subseq l1 l2
| subseq_intro : forall (l1 l2 : list X) (x : X),
              subseq l1 l2 -> subseq (x :: l1) (x :: l2).

Notation "l <<< k" := (subseq l k) (at level 10).

我试图证明这样一个引理：

Lemma …

假设我有以下结构

struct Test {
    value : i32,
}

我为它实现了以下方法

impl Test {
    fn take_ownership(self) -> Option<Self> {
       if self.value >= 0 {
           Some(self)
       } else {
           None
       }
    }
}

value我很擅长在大于 的情况下消耗所有权0，但是如何重写代码以便在None返回的情况下不消耗所有权？