在阿格达标准库，我们有RawMonad，RawApplicative等。
RawMonad : ∀ {f} → (Set f → Set f) → Set _
RawMonad M = RawIMonad {I = ⊤} (λ _ _ → M)
RawMonadZero : ∀ {f} → (Set f → Set f) → Set _
RawMonadZero M = RawIMonadZero {I = ⊤} (λ _ _ → M)
RawMonadPlus : ∀ {f} → (Set f → Set f) → Set _
RawMonadPlus M = RawIMonadPlus {I = ⊤} (λ _ _ → M)
他们为什么以Raw? 在那里Monad或Applicative在阿格达？
尼尔斯·安德斯·丹尼尔森（Nils Anders Danielsson）（我怀疑是他们的作者）曾告诉我，这是因为它们不包含相应法律的证明。AFAIK，Agda 标准库没有包含此类证明的这些版本，但如果您愿意，您可以推出自己的版本。
本文收集自互联网，转载请注明来源。
如有侵权，请联系 [email protected] 删除。
我来说两句