ΛВ
ну вот прдеставься, расскажи где работаешь
так не прокатит
Size: a a a
2021 March 14
R
примерно так: работает на всех конкретных выражениях, если внутри нет релевантных непрозрачных термов
а типа если внутри будет лежать нераскрытый терм?
R
или лучше пока остановица
R
просто немного ломает мозг сопоставлять компуты
R
то есть я могу короче спокойно
Compute orb false false. поменять на Check orb false false = false.?V
"не нужна тебе эта библиотека"
"братка, не нужна тебе эта библиотека"
AT
то есть я могу короче спокойно
Compute orb false false. поменять на Check orb false false = false.?Check eq_refl : orb false false = false.
ᛒ
Check eq_refl : orb false false = false.
AT
можешь пока "Check eq_refl : ” читать как “assert”.
R
Check eq_refl : orb false false = false.
а eq_refl это заранее определенное получаеца
AT
мы его скоро введём
R
Displays the type of termtermterm. When called in proof mode, the term is checked in the local context of the selected goal.
AT
If новая-зависимость then подумой!
R
получаеца eq_refl я и так могу втыкивать
R
мы его скоро введём
ну вот жалко что не рассказал или показал….
R
ну а как тогда компактно проверять то шо написал