Diğer yazarların Coq provalarını incelerken, sıklıkla bir taktikle karşılaşıyorum, "inv eq Heq" veya "intro_b" diyelim. Ben böyle taktikleri anlamak istiyorum.Coq provalarında bir taktiğin tanımını bulma
Güncel projemde bir yerde tanımlanmış bir Coq taktiği mi yoksa Taktiksel Gösterge mi olduğunu nasıl bulabilirim?
İkincisi, tanımını bulmanın bir yolu var mı?
Aramada Ara, Bul, Bul ve Yazdır, ancak yukarıdaki soruların yanıtlarını bulamadım.
Sen (documentation göre) kullanıcı tanımlı taktik kodunu yazdırmak için
Print Ltac <tacticname>.
kullanmak gerekir.
Locate görünüyor taktik adları için çalışmıyor grep ihtiyacımız olacak sanırım bulmak için.
Daha önce bahsedildiği gibi, Print Ltac ..., kullanıcı tanımlı bir taktik kodunu yazdırır.
Kullanıcı tanımlı bir taktiği bulmak için (yani tanımlandığı yeri öğrenmek için) Locate Ltac ... kullanın. Size tam nitelikli isim verir. Sonra ilgili dosyayı bulmak için Locate Library kullanın.
@SpaceBeers'ın taktik sürümüdür: Sanırım sadece kafanız karışık. Bu bir cevaptır, bir eleştiri ya da herhangi bir şekilde açıklama talebi değildir. –
Evet, tamam. Yanlış düğmeye bas. Yorum kaldırıldı. – SpaceBeers
@downvoter, lütfen yorum bırakın? –
'Bulun Ltac',' Locate' –