<commit_before>module Prelude.Pairs

import Builtins

%access public
%default total

using (a : Type, P : a -> Type)

    ||| Dependent pair where the first field is erased.
    data Exists : (P : a -> Type) -> Type where
        evidence : .(x : a) -> (pf : P x) -> Exists P

    ||| Dependent pair where the second field is erased. 
    data Subset : (a : Type) -> (P : a -> Type) -> Type where
        element : (x : a) -> .(pf : P x) -> Subset a P

    ||| The type class of dependent pairs.
    class DepPair (a : Type) (P : a -> Type) (T : Type) where

        ||| The first projection from a dependent pair.
        getWitness : (x : T) -> a

        ||| The second projection from a dependent pair.
        getProof : (x : T) -> P (getWitness x)

    instance DepPair a P (Exists {a} P) where
        getWitness (evidence x pf) = x
        getProof   (evidence x pf) = pf

    instance DepPair a P (Subset a P) where
        getWitness (element x pf) = x
        getProof   (element x pf) = pf

    instance DepPair a P (Pair a P) where
        getWitness (pair x pf) = x
        getProof   (pair x pf) = pf
<commit_msg>Fix indentation, use monomorphic projections for pairs.<commit_after>module Prelude.Pairs

import Builtins

%access public
%default total

using (a : Type, P : a -> Type)

  ||| Dependent pair where the first field is erased.
  data Exists : (P : a -> Type) -> Type where
    evidence : .(x : a) -> (pf : P x) -> Exists P

  ||| Dependent pair where the second field is erased. 
  data Subset : (a : Type) -> (P : a -> Type) -> Type where
    element : (x : a) -> .(pf : P x) -> Subset a P

  -- Monomorphic projections

  namespace Exists
    getWitness : Exists {a} P -> a
    getWitness (evidence x pf) = x

    getProof : (x : Exists {a} P) -> P (getWitness x)
    getProof (evidence x pf) = pf

  namespace Subset
    getWitness : Subset a P -> a
    getWitness (element x pf) = x

    getProof : (x : Subset a P) -> P (getWitness x)
    getProof (element x pf) = pf

  namespace Pair
    getWitness : Pair a P -> a
    getWitness (pair x pf) = x

    getProof : (x : Pair a P) -> P (getWitness x)
    getProof (pair x pf) = pf

  -- Polymorphic (class-based) projections have been removed
  -- because type-directed name disambiguation works better.

{'fraction_non_alphanumeric': 0.11514886164623468, 'fraction_numerical': 0.0, 'mean_word_length': 2.2596291012838803, 'pattern_counts': {'":': 0, '<': 3, '<?xml version=': 0, '>': 32, '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': '5875539', 'n_tokens_mistral': 792, 'n_tokens_neox': 754, 'n_words': 315}