Jestem nowym użytkownikiem Coq. Zdefiniowałem niektóre funkcje:Nie można użyć let-destruct dla krotki w Coq
Definition p (a : nat) := (a + 1, a + 2, a + 3).
Definition q :=
let (s, r, t) := p 1 in
s + r + t.
Definition q' :=
match p 1 with
| (s, r, t) => s + r + t
end.
Próbuję zniszczyć wynik p w reprezentacji krotki. Jednak coqc narzeka na q:
Error: Destructing let on this type expects 2 variables.
natomiast q 'może przekazać kompilację. Jeśli zmienię p, aby zwrócić parę (a + 1, a + 2), odpowiednie q i q 'działają bez zarzutu.
Dlaczego zezwala się tylko na zezłomowanie? Czy popełniłem błąd w składni? Sprawdziłem z podręcznikiem Coq, ale nie znalazłem żadnej wskazówki.
Dziękujemy!
Dziękujemy! Tak więc 3-członową krotkę należy uznać za niszczącą na pierwszym członku pary, a następnie muszę użyć "cytatu"? – xywang
Tak, to jest to! –