Есть ли в Изабель переписать такти c?

Question

Например, в Coq есть rewrite, и мы также можем поставить стрелки `<-: </p>

Inductive bool: Set :=
  | true
  | false.

Lemma equality_of_functions_commutes:
  forall (f: bool->bool) x y,
    (f x) = (f y) -> (f y) = (f x).
Proof.
  intros.
  rewrite H.
  reflexivity.
Qed.

source: https://pjreddie.com/coq-tactics/#rewrite

Answer 1

Я не верю, что он такой же сильный, как версия Coq, но

• саб, описанный в 5.8.1 старого урока и

• перезапись, показанная в примерах

теоремы перезаписи. Тем не менее, вы не можете легко переписать предположения в стиле применения.