No Pat.Meta

[HoshinoTented]

Code:

      open data Nat | O | S Nat
      open data List | nil | cons List
      -- [1, n]
      open data Fin (n : Nat)
      | S _ => F1
      | S n' => FS (Fin n')

      def length List : Nat
      | nil => O
      | cons xs => S (length xs)

      def get (xs : List) (Fin (length xs)) : Nat
      | nil, x => O
      | cons xs, F1 => S O
      | cons xs, FS x => S (S O)

Pat.Meta is not allowed

```plain Pat.Meta is not allowed org.aya.generic.util.InternalException: Pat.Meta is not allowed at app//org.aya.core.pat.PatMatcher.match(PatMatcher.java:79) at app//org.aya.core.pat.PatMatcher.match(PatMatcher.java:135) at app//kala.function.CheckedConsumer.accept(CheckedConsumer.java:46) at app//kala.collection.base.Traversable.forEach(Traversable.java:699) at app//kala.collection.base.Traversable.forEachChecked(Traversable.java:705) at app//org.aya.core.pat.PatMatcher.visitList(PatMatcher.java:131) at app//org.aya.core.pat.PatMatcher.match(PatMatcher.java:62) at app//org.aya.core.pat.PatMatcher.match(PatMatcher.java:135) at app//org.aya.core.pat.PatMatcher.tryBuildSubstTerms(PatMatcher.java:46) at app//org.aya.tyck.pat.PatTycker.mischa(PatTycker.java:533) at app//org.aya.tyck.pat.PatTycker.selectCtor(PatTycker.java:504) at app//org.aya.tyck.pat.PatTycker.doTyck(PatTycker.java:264) at app//org.aya.tyck.pat.PatTycker.updateSig(PatTycker.java:449) at app//org.aya.tyck.pat.PatTycker.visitPatterns(PatTycker.java:382) at app//org.aya.tyck.pat.PatTycker.checkLhs(PatTycker.java:178) at app//org.aya.tyck.pat.PatTycker.lambda$checkAllLhs$3(PatTycker.java:142) at app//org.aya.tyck.pat.PatTycker.traced(PatTycker.java:92) at app//org.aya.tyck.pat.PatTycker.lambda$checkAllLhs$4(PatTycker.java:140) at app//kala.collection.immutable.ImmutableVectors$Vector1.mapIndexed(ImmutableVectors.java:408) at app//kala.collection.immutable.ImmutableVectors$Vector1.mapIndexed(ImmutableVectors.java:162) at app//org.aya.tyck.pat.PatTycker.checkAllLhs(PatTycker.java:140) at app//org.aya.tyck.pat.PatTycker.elabClausesClassified(PatTycker.java:124) at app//org.aya.tyck.StmtTycker.lambda$doTyck$3(StmtTycker.java:93) at app//kala.control.Either$Right.fold(Either.java:332) at app//org.aya.tyck.StmtTycker.doTyck(StmtTycker.java:73) at app//org.aya.tyck.StmtTycker.traced(StmtTycker.java:54) at app//org.aya.tyck.StmtTycker.tyck(StmtTycker.java:61) at app//org.aya.tyck.TyckDeclTest.tyck(TyckDeclTest.java:35) at app//org.aya.tyck.TyckDeclTest.lambda$successTyckDecls$0(TyckDeclTest.java:58) at app//kala.collection.base.Iterators$3.next(Iterators.java:777) at app//kala.collection.base.Iterators$Filter.hasNext(Iterators.java:1706) at app//kala.collection.immutable.ImmutableVector.from(ImmutableVector.java:159) at app//kala.collection.immutable.ImmutableVector.from(ImmutableVector.java:140) at app//kala.collection.CollectionLike.toImmutableVector(CollectionLike.java:107) at app//kala.collection.CollectionLike.toImmutableSeq(CollectionLike.java:95) at app//org.aya.tyck.TyckDeclTest.successTyckDecls(TyckDeclTest.java:59) at app//org.aya.LocalTest.test(LocalTest.java:22) ```

[HoshinoTented]

The Core: The tycker visited the patterns of ctor without inline

[HoshinoTented]

Minimum Code, use this! @ice1000 :

      open data Nat | O | S Nat
      open data Foo Nat
      | O => foo0
      | S _ => foo1

      def justMatch {n : Nat} (Foo n) : Nat
      | foo0 => O
      | foo1 => S O