<commit_before>import Parametric.Syntax.Type as Type

module Parametric.Syntax.MType where

module Structure (Base : Type.Structure) where
  open Type.Structure Base

  mutual
    --  Derived from CBPV
    data ValType : Set where
      U : (c : CompType) → ValType
      B : (ι : Base) → ValType
      vUnit : ValType
      _v×_ : (τ₁ : ValType) → (τ₂ : ValType) → ValType
      _v+_ : (τ₁ : ValType) → (τ₂ : ValType) → ValType

    data CompType : Set where
      F : ValType → CompType
      _⇛_ : ValType → CompType → CompType
      -- We did not use this in CBPV, so dropped.
      -- _Π_ : CompType → CompType → CompType

  cbnToCompType : Type → CompType
  cbnToCompType (base ι) = F (B ι)<commit_msg>MType: Fix arity of _v×_<commit_after>import Parametric.Syntax.Type as Type

module Parametric.Syntax.MType where

module Structure (Base : Type.Structure) where
  open Type.Structure Base

  mutual
    --  Derived from CBPV
    data ValType : Set where
      U : (c : CompType) → ValType
      B : (ι : Base) → ValType
      vUnit : ValType
      _v×_ : (τ₁ : ValType) → (τ₂ : ValType) → ValType
      _v+_ : (τ₁ : ValType) → (τ₂ : ValType) → ValType

    -- Same associativity as the standard _×_
    infixr 2 _v×_

    data CompType : Set where
      F : ValType → CompType
      _⇛_ : ValType → CompType → CompType
      -- We did not use this in CBPV, so dropped.
      -- _Π_ : CompType → CompType → CompType

  cbnToCompType : Type → CompType
  cbnToCompType (base ι) = F (B ι)
{'fraction_non_alphanumeric': 0.09651474530831099, 'fraction_numerical': 0.0006702412868632708, 'mean_word_length': 2.4400921658986174, 'pattern_counts': {'":': 0, '<': 3, '<?xml version=': 0, '>': 3, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '2239400', 'n_tokens_mistral': 533, 'n_tokens_neox': 535, 'n_words': 192}