AFP의 'find_theorems`

Question

find_theorems 메커니즘을 사용하여 정식 교정 자료 (AFP) 전체 보관소를 검색하려면 어떻게해야합니까?

내 컴퓨터에 보관 파일을 다운로드했으며 여기에서 이론을 가져올 수 있습니다. 예를 들어, 내가 imports Kleene_Algebra.Kleene_Algebra_Models이라고 쓰면 그 이론의 모든 정리가 성공적으로 나에게 제공된다. 하지만 find_theorems <expression>을 입력하면 가져온 특정 이론의 검색 결과 만 표시됩니다. 전체 아카이브를 검색하려면 어떻게해야합니까? 예를 들어, 아마도 누군가가 나에게 유용한 정리를 증명했지만, 나는 그들이 그들의 이론이라고 부른 것을 모른다.

Answer 1

find_theorems은로드 된 이론에서만 작동합니다. 정리 이름에 대해 알고 있다면 텍스트 검색 도구를 사용할 수 있습니다. macOS에서는 스팟 라이트 검색 (cmd + space)이 유용 할 수 있습니다.

Answer 2

AFP 전체를 이론에 가져 오지 않는 한 간단하고 간단하게 말하면 안됩니다 (아마도 작동하지 않을 것입니다).

현재 누군가가 원하는 일을하고 있는지 여부를 확신 할 수 없습니다.