БОЛЬШОЙ кок

кому скажи 10 лет назад, что в агде тактики будут, в лицо рассмеются

это да)

сначала скалисты писали дсл
потом жейсоны
потом билд тулы
а теперь свои тредпулы

там еще где-то в середине тест тулы есть

Эх, сча бы есть

перел тредпулами

ты прав

@AntonTrunov на семинар, к сож, не попадаю - митинг - в записи послушою.

партсобрание, будем обсуждать, почему я в рабочее время коком балуюсь.

почему лайвстриму на ютабе можно менять скорость

ахах

я их там даже после упоминания не нашёл, впрочем

вот это вэлью в докладе Олега

20/10!

как понимаю, https://agda.readthedocs.io/en/v2.5.2/language/reflection.html

The comparison to tactics in a lan- guage like Coq is a tempting one, and we see both advantages and disadvantages of each style. Of course, the tactic language in Coq is much more specialised and sophisticated, but it is a pity that it is separate. This paper explores an alternative, with metaprograms written directly in the object language. Some people might also appreciate the fact that proof generation in Agda is explicit.

не, это в бородатом году в агде было

только в сравнении с коковскими тактиками tyazhelovato

It seems conceivable that in the future, using techniques such as those pre- sented here, a framework for tactics might be within reach. Eventually we might be able to define an embedded language in Agda, in the style of Coq’s tactic language, then inspect the shape of the proof obligation, and look at a database of predefined proof recipes to see if one of them might discharge or simplify the obligation. An advantage of this approach versus the tactic language in Coq, would be that the language of the propositions and tactics is the same.