man(1)

📦 version 1.3.4, in arch rolling, fedora 43, fedora 44

💖 man(1) — the idris manual, but make it a group chat 💖

okay bestie, you opened man(1) for idris and I am SO glad you did, because this language is genuinely iconic and you deserve to know everything about it. let's get into it 🫶

✨ NAME ✨

idris — a general purpose pure functional programming language with dependent types. yes that's the whole name section, she's short but she's powerful 💅

🌸 SYNOPSIS 🌸

idris [ options] [FILES]

🦋 DESCRIPTION 🦋

so. Idris is a general purpose pure functional programming language with dependent types. and when I say dependent types, I mean types can be predicated on values — which is lowkey the coolest thing ever, because it means some aspects of a program's behaviour can be specified precisely in the type. she's compiled, she uses eager evaluation, and her features are influenced by Haskell and ML. a nepo baby in the best way 💖

here's the full feature list, no skips, no cuts:

  • 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
⚠️ okay important thing, bestie, real talk: it is important to note that Idris is first and foremost a research tool and project. so the tooling provided and the resulting programs created should not necessarily be seen as production ready nor for industrial use. she's a research queen, not a corporate girlie. no cap.

🎀 OPTIONS 🎀

every single one, periodt:

  • --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
  • --listlogcats — Display logging categories
  • --link — Display link flags
  • --listlibs — Display installed libraries
  • --libdir — Display library directory
  • --include — Display the includes flags
  • --V2 — Loudest verbosity
  • --V1 — Louder verbosity
  • -V, --V0, --verbose — Loud verbosity
  • --ibcsubdir FILE — Write IBC files into sub directory
  • -i,--idrispath ARG — Add directory to the list of import paths
  • --sourcepath ARG — Add directory to the list of source search paths
  • -p,--package ARG — Add package as a dependency
  • --port PORT — REPL TCP port
  • --build IPKG — Build package
  • --install IPKG — Install package
  • --repl IPKG — Launch REPL, only for executables
  • --clean IPKG — Clean package
  • --mkdoc IPKG — Generate IdrisDoc for package
  • --checkpkg IPKG — Check package only
  • --testpkg IPKG — Run tests for package
  • -S,--codegenonly — Do no further compilation of code generator output
  • -c,--compileonly — Compile to object files rather than an executable
  • --codegen TARGET — Select code generator: C, Javascript, Node and bytecode are bundled with Idris
  • --cg-opt ARG — Arguments to pass to code generator
  • -e,--eval EXPR — Evaluate an expression without loading the REPL
  • --execute — Execute as idris
  • --exec EXPR — Execute as idris
  • -X,--extension EXT — Turn on language extension (TypeProviders or ErrorReflection)
  • --partial-eval — Switch on partial evaluation
  • --target TRIPLE — If supported the codegen will target the named triple.
  • --cpu CPU — If supported the codegen will target the named CPU, e.g. corei7 or cortex-m3.
  • --color,--colour — Force coloured output
  • --nocolor,--nocolour — Disable coloured output
  • --optimise-nat-like-types,--optimize-nat-like-types — Compile Nat-like types to big ints
  • --no-optimise-nat-like-types,--no-optimize-nat-like-types — Do not compile Nat-like types to big ints
  • --consolewidth WIDTH — Select console width: auto, infinite, nat
  • --highlight — Emit source code highlighting
  • --no-tactic-deprecation-warnings — Disable deprecation warnings for the old tactic sublanguage
  • -v,--version — Print version information
  • -h,--help — Show this help text

👑 SEE ALSO 👑

go forth and lurk, bestie:

💜 AUTHOR 💜

The Idris Community — collectively serving, as always 👑

and that's the whole page, babes 🌈 this manual was version 1.3.3, dated 23 May 2020, and it lives under man(1). go typecheck something, you got this 💖✨

📦 where this page comes from