小编Ger*_*ler的帖子

我正在创建一个插件，它将发出由套接字触发的基本 nuxt 事件。然后将收到 nuxt 事件并打开小吃店。当在组件内部时，很容易通过使用发送和接收事件$nuxt

this.$nuxt.$on('open-snackbar', this.handler)

this.$nuxt.$emit('open-snackbar', options)

但是，我如何尝试在插件中执行此操作，因此它不绑定到任何页面，而是存在于整个应用程序中。我似乎无法弄清楚如何从所述插件中发出它：

export default (context) => {
    console.log(context)
    console.log(context.$emit)
    console.log(context.emit)
    console.log(context.$nuxt)
    console.log(context.app.emit)
    console.log(context.app.$nuxt)
}

context.app似乎它是正确的对象，但它似乎不起作用。有任何想法吗？

我是COQ的新手,我试图证明反例定理.

Variable A B:Prop.

Hypothesis R1: ~A->B.
Hypothesis R2: ~B.

Theorem ej: A.

当我们研究逻辑时,我们学习了RAA技术,但在COQ中,这并没有增加新的假设,现在我们陷入困境.

那么我们尝试:

Proof.
tauto.
Show Proof.

有了以下输出,但我们不知道它是什么意思.

(NNPP A
   (fun H : ~ A => let H0 : B := R1 H in let H1 : False := R2 H0 in False_ind False H1))

有人可以帮我们理解COQ Show Proof输出吗？