<commit_before>.\" Manpage for Idris.
.\" Contact <> to correct errors or typos.
.TH man 1 "25 March 2016" "0.12.3" "Idris man page"
.SH NAME
idris -\ a general purpose pure functional programming language with dependent types.
.SH SYNOPSIS
idris [ options] [FILES]
.SH DESCRIPTION
Idris is a general purpose pure functional programming language with
dependent types. Dependent types allow types to be predicated on
values, meaning that some aspects of a program’s behaviour can be
specified precisely in the type. It is compiled, with eager
evaluation. Its features are influenced by Haskell and ML.

+ Full dependent types with dependent pattern matching
+ Simple case expressions, where-clauses, with-rule
+ Pattern matching let- and lambda-bindings
+ Overloading via Interfaces (Type class-like), Monad comprehensions
+ do-notation, idiom brackets
+ Syntactic conveniences for lists, tuples, dependent pairs
+ Totality checking
+ Coinductive types
+ Indentation significant syntax, Extensible syntax
+ Tactic based theorem proving (influenced by Coq)
+ Cumulative universes
+ Simple Foreign Function Interface
+ Hugs style interactive environment

It is important to note that Idris is first and foremost a research tool
and project. Thus the tooling provided and resulting programs created
should not necessarily be seen as production ready nor for industrial use.

.SH OPTIONS
  --nobanner               Suppress the banner
  -q,--quiet               Quiet verbosity
  --ide-mode               Run the Idris REPL with machine-readable syntax
  --ide-mode-socket        Choose a socket for IDE mode to listen on
  --ideslave               Deprecated version of --ide-mode
  --ideslave-socket        Deprecated version of --ide-mode-socket
  --log LEVEL              Debugging log level
  --logging-categories CATS
                           Colon separated logging categories. Use --listlogcats
                           to see list.
  --nobasepkgs             Do not use the given base package
  --noprelude              Do not use the given prelude
  --nobuiltins             Do not use the builtin functions
  --check                  Typecheck only, don't start the REPL
  -o,--output FILE         Specify output file
  --interface              Generate interface files from ExportLists
  --typeintype             Turn off Universe checking
  --total                  Require functions to be total by default
  --warnpartial            Warn about undeclared partial functions
  --warnreach              Warn about reachable but inaccessible arguments<commit_msg>Fixed formatting of man page.<commit_after>.\" Manpage for Idris.
.\" Contact <> to correct errors or typos.
.TH man 1 "25 March 2016" "0.12.3" "Idris man page"
.SH NAME
idris -\ a general purpose pure functional programming language with dependent types.
.SH SYNOPSIS
idris [ options] [FILES]
.SH DESCRIPTION
Idris is a general purpose pure functional programming language with
dependent types. Dependent types allow types to be predicated on
values, meaning that some aspects of a program’s behaviour can be
specified precisely in the type. It is compiled, with eager
evaluation. Its features are influenced by Haskell and ML.

+ Full dependent types with dependent pattern matching

+ Simple case expressions, where-clauses, with-rule

+ Pattern matching let- and lambda-bindings

+ Overloading via Interfaces (Type class-like), Monad comprehensions

+ do-notation, idiom brackets

+ Syntactic conveniences for lists, tuples, dependent pairs

+ Totality checking

+ Coinductive types

+ Indentation significant syntax, Extensible syntax

+ Tactic based theorem proving (influenced by Coq)

+ Cumulative universes

+ Simple Foreign Function Interface

+ Hugs style interactive environment

It is important to note that Idris is first and foremost a research tool
and project. Thus the tooling provided and resulting programs created
should not necessarily be seen as production ready nor for industrial use.

.SH OPTIONS
  --nobanner               Suppress the banner
  -q,--quiet               Quiet verbosity
  --ide-mode               Run the Idris REPL with machine-readable syntax
  --ide-mode-socket        Choose a socket for IDE mode to listen on
  --ideslave               Deprecated version of --ide-mode
  --ideslave-socket        Deprecated version of --ide-mode-socket
  --log LEVEL              Debugging log level
  --logging-categories CATS
                           Colon separated logging categories. Use --listlogcats
                           to see list.
  --nobasepkgs             Do not use the given base package
  --noprelude              Do not use the given prelude
  --nobuiltins             Do not use the builtin functions
  --check                  Typecheck only, don't start the REPL
  -o,--output FILE         Specify output file
  --interface              Generate interface files from ExportLists
  --typeintype             Turn off Universe checking
  --total                  Require functions to be total by default
  --warnpartial            Warn about undeclared partial functions
  --warnreach              Warn about reachable but inaccessible arguments
{'fraction_non_alphanumeric': 0.0508507347254447, 'fraction_numerical': 0.004253673627223511, 'mean_word_length': 2.607391910739191, 'pattern_counts': {'":': 0, '<': 5, '<?xml version=': 0, '>': 5, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 2, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '5642241', 'n_tokens_mistral': 1318, 'n_tokens_neox': 1222, 'n_words': 613}