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

import rules scala://sequences.mmt.kwarc.info❚

theory Sequences =
   include ?Typed❙
   include ?Nat❙

   rep # 1 ^ 2 prec -20❙
   rule rules?NTypeTerm❙
   rule rules?UniverseNType❙

   ellipsis  # ⟨' 2 | V1T '⟩ prec -10002 ❙
   index     # 1 .. 2 prec 9998 ❙
   flatseq   # ⟨ 1,… ⟩ prec 0❙
   
   foldLeft # foldL 1 2 3 4 ❙

   rule rules?EllipsisInfer❙
   rule rules?EllipsisTypeCheck❙
   rule rules?EllipsisEqualityCheck❙
   rule rules?EllipsisInjective❙
   rule rules?RepTypeCheck❙
   rule rules?RepEqualityCheck❙
   rule rules?ExpandRep❙
   rule rules?IndexInfer❙
   rule rules?IndexCompute❙
   rule rules?FlatseqInjective❙
   rule rules?SolveArity❙
   rule rules?LengthAwareApplyTerm❙
   rule rules?LengthAwareBeta❙
   rule rules?FoldLeftType ❙
❚

theory LFS =
   include ?DHOL❙
   include ?Sequences❙
  
   rule rules?FlexaryPi❙
   rule rules?FlexaryLambda❙
   rule rules?FlexaryApply❙
❚