►
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
Okay
branch
create
origin,
main
2002.08
coherence
yeah,
so
we
wanted
to
get
around
to
modeling
negative
impulse,
but
before
we
can
do
that,
we
kind
of
need
to
have
the
coherence
check.
I
think
a
little
more
accurate.
So
maybe
we
can
start
with.
Currently
we
have
the
orphan
rules
which
are
incomplete
and
we
don't
have
any
overlap.
Rules.
B
A
A
So
we'll
start
by
making
a
new.
Let
me
just
page
some
of
this
back
in
so
we've
got
this.
This
is
the
main
checking
like
judgment.
It
says
the
whole
program
is
checked.
If
all
this
stuff
is
true,
and
one
of
them
is
that
we
check
every
crate
item
is
defined
here
and
here's
the
rules
for
checking
different
items.
A
A
A
B
B
A
A
B
A
B
A
A
A
A
A
A
A
Okay,
let
me
show
you
what
I
just
did
so
so
this
function.
The
select
trade
item
takes
a
single
crate
item
which
could
be
anything
and
returns
a
list
of
either
empty
list
or
or
a
one
item
list
right
and
here
we're
using
these
crazy
patterns
to
say
for
each
crate
and
then
within
each
crate,
for
each
item
and
kind
of
flatten.
A
A
A
A
B
A
Basically,
what
I
was
thinking
is:
if
we
can,
we
should.
We
know
that
this
this
impul
has
to
appear
at
least
once
in
this
list,
so
we
could
find
all
the
things
we
could
find.
The
first
such
appearance
or
any
such
appearance
really
and
then
find
all
the
things
that
come
before
and
all
the
things
that
come
after
and
if
it
appears
more
than
once,
it'll
be
in
one
of
those
two
lists
right,
and
so
as
long
as
we
pair
it,
I
think
it
doesn't
actually
matter
kind
of
which
one
it
originally
was.
A
A
A
A
A
A
A
A
Like
where
there's
a
list
of
exactly
what
length
one
that
sort
of
of
where
you
you
filter
down
to
only
impulse
that
are
exactly
equal
to
this
and
the
result
should
be
of
length
one
something
like
that
anyway.
So
now
we
have
the
more
interesting
case
where
there's
two
impulse-
and
I
guess
the
next
thing
I
would
point
out-
is
we
haven't
actually
looked
at
what.
A
A
B
A
So
and
now
we
are
extracting
the
name
of
the
trait
extracting
all
the
impulse
of
that
trait,
and
I'm
not
sure
why
this
is
in
a
list.
That's
not
right
all
the
impulse
of
the
tree
getting
a
big
list
of
impulse
and
then
we're
matching
across
them.
So
now
we
know
that
these
two
they
ought
to
be
of
the
same
trait
for
sure.
A
A
A
A
A
A
A
A
A
A
The
meta
functions
are
just
sort
of
regular
functions
and
then
the
judgment
forms
are
more
like
prolog
predicates.
That
kind
of
do
search
right,
and
so,
if
you
invoke
one
when
you,
you
can
check
whether
a
judgment
holds
and
what
you
get
back
is
like
a
list
of
values
for
which
it
holds
and
if
that's
the
empty
set,
then
it
doesn't
hold.
A
A
A
A
So,
jumping
back
to
context,
we
want
to
show
we'll
start
with
this.
We
want
to
prove
that
these
parameters
see,
if
they're,
equal
or
not
right,
and
it's
only
want
this
to
be
valid
if
they
cannot
be
made
equal,
so
we
have
to
create
for
each
of
these,
these
kind
of
var
ids
correspond
to
the
generics
on
the
impul.
We
need
to
instantiate
them
with
inference
variables
and
then
try
to
unify
essentially.
A
A
A
A
A
A
A
B
A
A
A
A
A
I'll
try
to
remember
now
how
this
works
right,
so
this
is
getting
into
the
the
weeds
of
red
x,
but,
like
we
have
these
judgments
and
we
have
these
meta
functions
that
are
pure
functions
that
always
return
a
result,
and
these
return
many
results
and
there's
a
you
can't
like
connect
them
directly,
but
you
can
call
this
function.
Judgment
holds.
A
A
A
A
Yes,
okay,
so
this
is
going
to
try
to
prove
this,
which
says
this
weird
name
is
the
name
of
the
solver
invoke
the
solver
on
the
given
environment
with
this
goal,
and
if
it
comes
back
with
anything
here
like
end
out,
that's
the
success.
That
means
it
succeeded
and
it
created
a
new
environment
that
contains
whatever
like
constraints
or
bindings
on
the
inference
variables
or
whatever
else
had
to
be
true.
For
this
goal
to
be
provable.
A
A
So
this
is
going
to
yield
a
list
of
solutions
each
one
of
which
is
going
to
be
an
environment
right.
So
if
it
was
successful,
it
could
be
like
environment,
one
environment,
two
environment,
three,
but
we're
gonna
check
that
it's
an
empty
list
and
I
guess
we
can
actually
we
don't
really
need
the
helper
function
to
do
this.
We
can
actually
do
this
here.
A
A
A
It
depends
on
your
assumptions
right,
like
first
of
all,
your
approver
might
just
not
be
that
smart,
and
so
maybe
something
is
provable,
but
it
can't
find
the
right
solution
to
prove
it
in
now.
In
our
case,
we
know
that,
like
the
ways
that
rust
can
prove,
things
are
limited,
so
we
don't
have
to
worry
about
that.
It's
considered
complete
meaning.
A
It
just
means
that
there
might
be
types
for
which
it
does
and
there
might
be
types
for
which
it
doesn't.
So.
My
point
is
the
fact
that
we
can't
prove
things
like
you
have
to
the
reason.
We're
kind
of
careful
with
this-
and
we
don't
just
want
to
add
a
general
purpose
negation
operator
to
rust-
is
that
you
have
to
interpret
it.
A
A
A
A
A
A
A
A
A
A
Right,
I
guess
now
I
realize
the
last
thing
I'll
do
is
we
don't
actually
need
the
biff
buy
formulas?
We
don't
need
in
this
particular
case,
because
those
would
be
useful
if
we
were
going
we'll
need
them
in
other
other
ones
where
like.
If
the
parameters
are
unifiable
we'll
need
them
so
that
we
can
go
find
if
any
of
the
where
clauses
cannot
be
proven.