namespace http://cds.omdoc.org/examples❚

theory FOLPatterns : ur:?LFS =
  include ?FOL❙
  
  pattern fun(n:NAT)❘# L1 : 2 ❘=
    f: term^n ⟶ term❙
  ❚
❚

theory Monoid : ?FOLPatterns =
  fun comp : 2❙
❚