Поиск фактов в Айсбахе - PullRequest
Новая
       37

Поиск фактов в Айсбахе

0 голосов
/ 19 марта 2020

Я хочу написать метод Эйсбаха, образец которого соответствует фактам, сообщенным print_facts. Тем не менее, я не могу понять название этого (динамического c) набора фактов.

Пример: 

proof
  {
    fix A B
    have "A ⟶ A" by simp
    have "B ⟶ B" by simp
    print_facts
  }
qed

Вывод print_facts: 

local facts:
  ??.<unnamed>:
      A ⟶ A
      B ⟶ B
  this: B ⟶ B

«Локальные факты» представляются набором установленных в настоящее время фактов в Изар доказательство. Из метода Эйсбаха я могу получить доступ к this через имя method_facts. Но как мне сопоставить факты в наборе ??.<unnamed> из Айсбаха?

...