에 목표를 계산합니다,하지만 난 "쿼드"의 정의를 기억하지 않고 내가 그 정의의 검색을 시작하고 싶지 않아요. 빠르게 쿼드를 정의로 대체 할 수있는 전술이 있습니까? Record quad (X Y:Type):= { x:X; y:Y}.
아니면 내가 기억하고 refine (@Build_quad _ _).
사용할 수 있나요?
Coq에서 레코드의 평등성을 증명하려고 시도 할 때 해당 필드를 모두 평등하게 분해하는 전술이 있습니까? 예 : Record R := {x:nat;y:nat}.
Variables a b c d : nat.
Lemma eqr : {|x:=a;y:=b|} = {|x:=c;y:=d|}.
a = c /\ b = d으로 줄일 수있는 방법이 있습니까? 일반
Coq 다시 쓰기 전술 계수 법과 결합력 (aac_tactics)을 테스트하고있었습니다. 다음 예제에서는 정수 (Z)에 대해 작동하지만 정수가 이터 리 (Q)로 바뀌면 오류가 발생합니다. Error: Tactic failure: No matching occurence modulo AC found. 관련이있는 것으로 밝혀졌다 Z 및 Q 간의 불일치 유사한 문