<commit_before>module Prelude.Basics

import Builtins
       
Not : Type -> Type
Not a = a -> Void

||| Identity function.
id : a -> a
id x = x

||| Manually assign a type to an expression.
||| @ a the type to assign
||| @ x the element to get the type
the : (a : Type) -> (x : a) -> a
the _ = id

||| Constant function. Ignores its second argument.
const : a -> b -> a
const x = \v => x

||| Return the first element of a pair.
fst : (s, t) -> s
fst (x, y) = x

||| Return the second element of a pair.
snd : (a, b) -> b
snd (x, y) = y

infixl 9 .

||| Function composition
(.) : {a, b, c : Type*} -> (b -> c) -> (a -> b) -> a -> c
(.) f g x = f (g x)

||| Takes in the first two arguments in reverse order.
||| @ f the function to flip
flip : (f : a -> b -> c) -> b -> a -> c
flip f x y = f y x

||| Function application.
apply : (a -> b) -> a -> b
apply f a = f a

||| Equality is a congruence.
cong : {f : t -> u} -> (a = b) -> f a = f b
cong Refl = Refl

||| Decidability. A decidable property either holds or is a contradiction.
data Dec : Type -> Type where

  ||| The case where the property holds
  ||| @ prf the proof
  Yes : {A : Type} -> (prf : A) -> Dec A

  ||| The case where the property holding would be a contradiction
  ||| @ contra a demonstration that A would be a contradiction
  No  : {A : Type} -> (contra : A -> Void) -> Dec A

<commit_msg>Remove Type* on type of (.)<commit_after>module Prelude.Basics

import Builtins
       
Not : Type -> Type
Not a = a -> Void

||| Identity function.
id : a -> a
id x = x

||| Manually assign a type to an expression.
||| @ a the type to assign
||| @ x the element to get the type
the : (a : Type) -> (x : a) -> a
the _ = id

||| Constant function. Ignores its second argument.
const : a -> b -> a
const x = \v => x

||| Return the first element of a pair.
fst : (s, t) -> s
fst (x, y) = x

||| Return the second element of a pair.
snd : (a, b) -> b
snd (x, y) = y

infixl 9 .

||| Function composition
(.) : (b -> c) -> (a -> b) -> a -> c
(.) f g x = f (g x)

||| Takes in the first two arguments in reverse order.
||| @ f the function to flip
flip : (f : a -> b -> c) -> b -> a -> c
flip f x y = f y x

||| Function application.
apply : (a -> b) -> a -> b
apply f a = f a

||| Equality is a congruence.
cong : {f : t -> u} -> (a = b) -> f a = f b
cong Refl = Refl

||| Decidability. A decidable property either holds or is a contradiction.
data Dec : Type -> Type where

  ||| The case where the property holds
  ||| @ prf the proof
  Yes : {A : Type} -> (prf : A) -> Dec A

  ||| The case where the property holding would be a contradiction
  ||| @ contra a demonstration that A would be a contradiction
  No  : {A : Type} -> (contra : A -> Void) -> Dec A


{'fraction_non_alphanumeric': 0.1615864854939405, 'fraction_numerical': 0.0007344840249724568, 'mean_word_length': 2.379652605459057, 'pattern_counts': {'":': 0, '<': 3, '<?xml version=': 0, '>': 68, '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': '4099243', 'n_tokens_mistral': 1002, 'n_tokens_neox': 972, 'n_words': 453}