►
From YouTube: Idris (Lightning Talk) — Caleb Jones
Description
No description was provided for this meeting.
If this is YOUR meeting, an easy way to fix this is to add a description to your video, wherever mtngs.io found it (probably YouTube).
B
A
Are
functions
that
make
a
value,
so
this
takes
basically
on
the
rough
side
that
says
this
is
a
function
that
takes
a
tee
and
another
list
and
makes
a
list
and
type
declarations
look
the
same,
and
we
can
do
the
same
kind
of
code
here.
So
this
is
a
tweaks
on
map,
so
we
can
find
some
types
that
we
can't
define
and
rust
in
Idris.
So
this
is
a
type
which
not
only
have
is
generic
over
some
type.
It's
generic
over
a
number-
and
here
our
nail
here.
A
Our
empty
list
has
0
things
in
it
and
our
constructor
here
that
makes
a
bigger
list,
takes
something
and
a
list
of
n
things
and
makes
a
list
of
n
plus
1
things.
So
with
this
we
can
say
like
this
is
a
list
of
three
integers
and
if
we
try
to
put
four
integers
in
there,
we'll
get
a
type
error
down
at
the
bottom
here
same.
If
we
put
to
its
saying
zero
is
not
equal
to
1
because
it
counts
down
from
there.
A
A
Let
me
go
back
a
moan
up
here.
The
way
we
define
functions
is
basically
every
function
starts
with
a
match.
So
we
say
the
sum
of
an
empty
list
is
zero.
The
sum
of
something
a
list
with
at
least
one
thing
is
that
first
thing
plus
other
stuff.
So
it's
like
the
match
block
inside
our
function
here
so
here,
because
we
know
that
we
have
at
least
one
thing
in
our
list.
We
only
have
to
put
one
arm
in
the
match:
block
the
other.
A
One
doesn't
exist
because
there's
no
empty
list
with
one
thing
in
it,
and
so
if
we
try
here
our
sample,
that
would
be
first
right.
A
B
A
Might
have
to
convince
this
that
this
has
at
least
one
thing
in
it
right
now
I'm
going
to
skip
over
that,
because
I
didn't.
I
didn't
prepare
that
part
there,
because
the
compiler
knows
a
lot
of
stuff
about
our
code.
It
can
write
a
lot
of
code
for
us,
so
if
you
know
zip
in
r
us
to
combine
two
iterators
into
pairs,
we
can
write
a
similar
function
here.
A
That
lets
us
apply
functions
over
the
pairs,
but
in
rust
you
have
to
know
what
happens
when
those
two
iterators
are
different
lengths
I
think
it
probably
just
stops
sooner
here,
since
we
have
the
same
n
in
all
these.
We
it
knows
that
you
have
to
have
two
lengths
of
the
same
to
list
of
the
same
length.
So
I
asked
it
to
split
our
cases
here.
It
knows
that
they're
the
same
empty
list,
and
here
it
knows
that
if
one
list
has
something
in
it,
they
both
have
to
have
something
in
it.