Bir taktik taktirindeki hata seviyesini artırma

Question

Ltac'de karmaşık bir taktik uygularken, başarısız olmasını beklediğim ve beklendiği (örneğin, repeat'u sona erdirmek veya geri dönüşe neden olmak için) bazı Ltac komutları veya taktik çağırma vardır. Bu başarısızlıklar genellikle başarısızlık seviyesinde çevreleyen try veya repeat blok “kaçış” daha üst düzeyde gündeme 0.

Hataları kaldırdı ve beklenmedik arızaları sinyal yararlı olmaktadır.

Eksik olduğum şey, bir taktiği tac çalıştırmak ve başarısızlık iletisini koruyarak daha yüksek bir düzeyde olmak üzere 0 düzeyinde bile hatasını işleme koymanın bir yoludur. Bu, benim tarafımda bir Ltac programlama hatası nedeniyle repeat'un sonlandırılmamasını sağladı.

Ltac'de böyle bir başarısızlık düzeyini yükselten yüksek dereceli bir taktiği uygulayabilir miyim?

Answer 1

Bunu Ocaml'de gerçekleştirmek için bir taktik yazabilirsiniz. Bunu GitHub here'a koyuyorum. Aşağıdaki sessizce başarı yerine bir hata artırmalıdır Örneğin

:

repeat (match goal with 
      | [ |- _ ] => 
      raise_error_level (assert (3 = 3) by idtac) 
     end). 

Answer 2

senin ne istediğini tam olarak elde etmenin mümkün olup olmadığını bilmiyorum, ama ben bazen aşağıdaki deyim kullanın: İlk taktik 0 seviyesine sahip başarısız olursa, || çalıştırmayı dener

tactic_expression_that_may_fail_with_level_0 
|| fail 1000 "There was some problem here" 

İkincisi, çok yüksek bir seviyede başarısız olacak ve size rapor edecektir. Başka bir tekniğin daha uygun olup olmayacağını görmek için somut bir kullanım belgesi sunabilirseniz, bu yardımcı olacaktır.