idris 2

Implicit arguments

From here:

names which begin with a lower case letter are automatically bound as implicit arguments in types

Dependent pairs

https://idris2.readthedocs.io/en/latest/tutorial/typesfuns.html#dependent-pairs

Two values. First value can show up in the second.

Eg: an implementation of Vector:

(n:Nat ** Vector n Int)

Multiplicty

Every variable has a multiplicty associated with it.
Courtesy of Quantitative Type theory (QTT) on which idris2 is based.
A concept apparently not there in idris1??

Values:

0: Erased at runtime
1: Used exactly once at runtime
Unrestricted: Can be used any number of times at runtime

Explicit multiplicity examples:

(0 n: Nat)
(1 n: Nat)

Default multiplicity values:

No multiplicity annotation => unrestricted
Implicit argument => 0

Fun fact: Following is a function that cannot be realized as it requires two instances of a but only 1 is allowed:

duplicate : (1 x:a) -> (a, a)

https://idris2.readthedocs.io/en/latest/tutorial/multiplicities.html

REPL

:?: show help
:import: import modules
:t: show type of a value
:ti: show type (including implicit arguments) of a value

λΠ> :doc **
Used to build dependent pairs together with parentheses

vim plugin: idir

Plugin seems not so maintained: https://github.com/edwinb/idris2-vim
This is for idris1 apparently: https://github.com/idris-hackers/idris-vim

Reload buffer	\|̊
Case split	\|̧