Meta.Append

1Lab

  • Types with concatenationπŸ”—


This page was written by AmΓ©lia Liao

back to index
open import 1Lab.Type
module Meta.Append where

Types with concatenationπŸ”—

record Append {β„“} (A : Type β„“) : Type β„“ where
  infixr 8 _<>_

  field
    mempty : A
    _<>_   : A β†’ A β†’ A

open Append ⦃ ... ⦄ public