'da özel proverizat taktikleri Doğru bir şekilde anlıyorsam (esas olarak applyTactic işlevinin varlığından), Idris'da teorem geliştirici için özel taktikler yazmak mümkündür. Nasıl yapılacağını öğrenmek için kullanabileceğim bazı örnekler nelerdir?Idris
Idris'da özel taktikler yazmak için iki mekanizma vardır: üst düzey ve düşük seviyeli yansıma.
Üst düzey yansıma kullanarak, değerlendirilen veriler yerine sözdizimi üzerinde çalışan bir işlev yazarsınız - bu, bağımsız değişkenini azaltmaz. Bu işlevler, Idris'daki mevcut taktikleri kullanarak tanımlanan yeni bir taktik döndürüyor. Bir prova şartını doğrudan iade etmek isterseniz, her zaman Exact'u kullanabilirsiniz. Bu tür yansımaların bir örneği the effects library'da bulunabilir. Yüksek düzey yansıma taktikleri, ispat modunda byReflection kullanılarak çağrılır.
Düşük seviyeli yansımada, doğrudan İdris'in çekirdek tipi kuramından alıntılanan şartlarla çalışırsınız. Bir taktik daha sonra TT -> List (TTName, TT) -> Tactic ilk argümanın hedef türü, ikincisi yerel ispat içeriği ve geri dönüş sonucu yüksek düzey yansıma ile aynıdır. Bu, laughadelic'in above'a bağlandığı durumdur. Bunlar, ispat modunda applyTactic kullanılarak çağrılmaktadır.
Nasıl yazılacağını ve nasıl kullanılacağını bilmiyorum ama yakın zamanda gördüm [özel taktik örneği] (https://github.com/idris-lang/Idris-dev/blob/master /libs/base/Data/Vect.idr#L18-L22) ve [kullanımının bir örneği] (https://github.com/idris-lang/Idris-dev/blob/master/libs/base/Data/ HVect.idr # L57). Umarım bu yardımcı olur. – laughedelic
Öyle, teşekkürler. –
Yukarıdaki linkler artık geçerli değil çünkü repo'nun HEAD'sine atıfta bulunuyorlar. Lütfen bunun yerine buraya bakın: [ilk] (https://github.com/idris-lang/Idris-dev/blob/10ef56b8c1629347ab213e97bfff551ee27e11d0/libs/base/Data/Vect.idr#L18-L22), [saniye] (https: //github.com/idris-lang/Idris-dev/blob/fb6a0ed1ad5e3acc3795d7ab674977bdb419129a/libs/base/Data/HVect.idr#L57) –