►
From YouTube: A Mir Formality walkthrough (2022-06-29)
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).
A
A
A
And
see
we're
throwing
in
some
unknown
items
for
extern
crates
and
things
it's
got
a
static.
I
was
going
to
ask
whether
it
includes
types,
but
maybe
the
example
doesn't
have
any
types
that
are
interesting.
B
To
apply
the
user
type
like
the
user
type
function,
to
convert
the
like
ones
and
texts
to
the
other.
Oh
okay,
like
the
user,
try
syntax
because
it
might
be
easier
to
read.
I
guess.
A
Yeah,
I
think
that
makes
sense
you
should
in
fact
I
plan
to
modify
the
declarations
to
just
take
user
types
directly
and
not
so
you
don't
even
need
this.
This
would
just
be
what
you
would
write,
but
I'm
wondering
normally.
I
guess
I
would
expect
this
to
be
in
a
term
declaration
like
just
wrap
this
in
term
or
wrap
this
actually.
B
Actually,
I
have
also
one
like
function,
which
generates
like
the
like
that
vertex
slot
syntax
and
there
it's
like
wrapped
in
term.
A
A
B
A
This
looks
really
cool,
I
don't
know,
I
don't
guess
this
kind
of
looks
like
exactly
what
I'm
was
hoping
to
get
have
you
tried
to
run
these
tests
and
see
what
happens.
B
B
Yeah
also
like
one
of
the
main
issues
right
now,
I
think
is
like
the
the
lifetimes
in
mir,
because
I'm
not
sure
like
like
right
now.
It's
all
fresh
variables,
but
I
guess
like
like
for
the
type
checking
we
want
the
unified
version
where
there
is
like
not
one
variable
for
like
each
lifetime,
so
like.
A
I
don't
think
so.
I
mean
that's
at
least
how
the
borrow
checker
works
now.
Is
that
it
it
sort
of
figures
everything
out,
so
it
doesn't
have
any.
A
B
I
mean
like
right
now
the
type
check
and
mir
like
as
it
is
implemented
in
the
formality.
It
expects
like
lifetimes
to
be
equal
between
the
local
declarations
and
like
a
rough
r
value,
for
example.
I
think-
and
this
is
not
the
case
right
now,
because
it
wasn't
like
any
borrower
out
who,
like
the
life,
tends
to
be
equal
or.
A
D
C
A
This
example
through
and
make
it
work
I
mean
it's
already
great
to
have
like
honestly,
you
know
just
just
writing.
This
was
like
sufficiently
time
consuming
that
I
didn't
want
to
get
around
to
it.
You
know,
even
though
it's
such
a
simple
little
bit
of
code,
but
I
guess
I
see
we
have
some
things
like
unknown
r
value
here
and
so
on.
What's
missing
are
there?
Is
there
a
little
list
of
like
the
missing
things
from.
A
D
A
A
I
thought
we
would
spend
more
time,
but
it
seems
like
you
made
more
progress
than
I
expected.
I
guess
the
thing
is:
should
we,
why
don't?
We
should
probably
merge
it
into
the
mirror,
formality
repo.
I
think.
B
Another
thing
that
we
could
do
is
add
the
like
unknown
stuff
to
the
grammar
for
now,
so
we
can
just.
A
A
I
think
we
should
add
it
to
the
grammar.
I
know
we
just
have
to
extend
the
type
checker
to
handle
it.
B
Yeah,
okay
and
also
a
lot
of,
and
I'm
not
sure
whether
we
need
to
extend
the
like
handling
of
constants
in
the
formality,
because,
right
now,
it's
only
numbers
right.
A
A
A
Let
me
pull
up
the
code,
I'm
wondering
did
anybody
so
I
had
those
various
pr's
open
and
I
don't
know
if
anyone
ever
had
a
chance
to
look
at
them.
If
either
of
any
of
you
did,
I
guess
it's
fine,
if
not
I'm
just
trying
to
decide,
what's
the
most
effective
way
to
get
more
of
a
reviewing
culture
here
and
less
of
a
nico
push's
code,
culture.
A
B
A
Okay,
cool,
I
think
I'll
start
to
merge
them,
but
I'll
just
keep
doing
that
same
habit.
Feel
free
to
you
know
if
you
don't
remember
or
call
if
you
left
a
comment
or
not
dominic
but
feel
free
to
leave
one
saying
check,
plus
or
something
that's
always
good.
So
all
right,
we
were
going
to
look
at
the
normalized
to
inductive
thing.
A
So
I
have
this
example,
which
I
don't
know.
Maybe
you
said
you
tried
to
reproduce
it
and
weren't
able
to
dominic,
but
the
idea
would
be
if
you
had
a
foo
item
and
a
bar
item
and
you
direct
them
to
one
another
so
that
foo
item
expands
to
bar
item
and
barium
expands
to
flu
item,
and
then
you
try
to
prove
it
equal
to
something
well
that
hopefully
won't
work,
but
with
the
way
the
createsolver
is
today.
I
think
it
should
work
because
you
should
be
able
to
normalize.
A
That
will
normalize
to
bar,
which
will
normalize
tofu,
which
will
create
a
cycle
and
since
right
now
we
consider
all
cycles
acceptable.
That's
a
problem,
but
okay,
here
cool.
However,
we
don't
want
that.
But
then
again
maybe
I'm
wrong
and
it's
not
proving
so.
Let's
see
why
it's
not
proving
either,
because
this
test
isn't
right
or
because
there's
some
other
reason
that
I
don't
know.
A
So
let
me
pull
up
the
xcode
or
whatever.
This
browser
is
that
I
use
or
code
editor
vs
code.
A
D
A
A
A
D
D
A
C
A
A
These
days,
which
is
to
say,
not
sure
if
that's
the
right
function
actually
but.
A
And
instead
of
encapsulating
that
the
test
equals-
and
it's
mostly
because
I
get
a
better
line
number
out
when
you
not
better-
take
quick
tickles,
you
get
a
better
line
number
out
when
the
test
doesn't
work.
A
We
just
take
indirectly
the
create
decals
and
the
create
id.
D
A
A
I
don't
seem
to
need
that,
and
we
don't
know
if
we
need
this
okay.
I
don't
always
trust
these
like
unused
annotations,
they've
they've
been
wrong
for
me
before.
Okay.
A
So
what
did
I
say
we
should
do
to
fix
it.
I
said
we
can
oh
right,
we
right
right
right,
so
the
the
logic
solver.
A
It's
currently
either
it's
called
proof,
slash
co-inductive
and
it's
either
plus
or
it's
minus,
and
if
it's
plus
we're
allowed
to
treat
it
like
a
co-inductive
predicate
and
if
it's
minus
or
not-
and
essentially
that
means
does
a
cycle,
is
a
cycle
true
or
not,
and
so
what
we
say
right
now
is
that
for
all
predicates,
in
which
we
kind
of
got
them
from
the
user,
all
user
predicates
are
plus,
but
everything
we
take
out
of
the
environment,
all
the
like,
if
we
use
a
where
clause
to
prove
it,
it's
minus
and
that's
because
the
the
idea
of
the
environment
is
that,
essentially
all
those
facts
came
from
the
outside.
A
So
if
we
were
to
depend
on
something
in
the
environment,
which
is
only
true
because
of
something
we
proved
independently,
then
that
creates
a
a
kind
of
opportunity
to
have
these
these
cycles.
We
want
basically,
basically,
in
that
case
our
caller
said.
If
you
can
prove
x,
then
y
is
true
and
they
should
have
been
able
to
prove
it
for
themselves.
A
It's
kind
of
the
intuition,
but
what
I
want
to
do-
and
we
want
to
change
this,
so
this
is
not
hardcoded
to
plus,
but
so
that
it
kind
of
depends
on
what
kind
of
predicate
we
have
and
actually
before
we
fix
this,
I'm
going
to
merge
one
of
these
pr's,
because
I
want
to
base
it
on
the
work
in
that
pr.
A
Now,
when
I
see
you
left
a
few
suggestions,
I'll
just
commit
that,
because
I
added
some
concepts
that
I'd
rather
not
have
to
rebase
over.
So
let
me
just
pull
that
in.
A
Okay,
so
right
now,
we've
got
right,
so
we
still
have
in
this
branch.
We
have
this
extra
clause.
This
is
the
one
I
wanted.
A
We
kind
of
have
a
plus
if
it's
a
predicate,
that
we
got
from
goals
or
we
have
this
idea
of
a
built-in
predicate
or
we've
got
the
minus
when
we
came
from
the
hypothesis,
and
so
I
want
to
do
something
a
little
more
sensitive
here
where
we
look
at
this
predicate
and
we
decide
well,
which
one
is
it:
is
it
a
co-inductive
one
or
not,
and
then
we
can
say
normalizes
2
is
not
co-inductive
and
it
should
solve
the
problem,
and
the
thing
I
was
observing
in
this
issue
is
that
we
already
have
a
bunch
of
these
little
like
the
logic.
A
Solver
doesn't
actually
know
the
syntax
of
predicates.
It
just
treats
them
like
an
opaque
term,
so
it
already
has
these
functions
that
it
can
call
to
ask
questions
like.
Is
this
a
predicate
even
because
it
doesn't
know
what
the
grammar
for
a
predicate
is,
and
is
it
a
built-in
one
and
is
it
a
relation
we
have
down
here,
which
is
when
you
have
like
a
subtype
of
b,
and
I
was
thinking
we
could
merge
all
these
little
boolean
functions
into
one
function.
A
That
said
categorize
this
goal
into
one
of
various
categories
and
the
categories
would
be
like
predicate
built-in,
predicate
relation
or
other
basically
like.
So
that's
what
I
wanted
to
do
as
a
refactoring
and
then
we
can
change
it
so
right
now
these
are
the
grammar
of
goals.
A
At
the
logic
level,
a
goal
is
either
an
atomic
goal,
which
is
like
a
predicate
or
a
relation
or
it's
one
of
these
built-in
connectives,
like
all
any
implies
quantifier.
But
if
you
go
to
predicate
you
just
get
any
term,
that's
why
we
have
to
have
this
classifier,
so
we
can
add
in
something
like
goal.
Classification
is.
A
User
predicate
for
now,
we'll
just
add
in
different
categories,
built-in
predicate
built-in
relation
or
connective
or
like
built-in
yeah.
I
guess
built-in
goal.
D
A
D
A
A
Okay,
so
what
does
this
do?
This
is
kind
of
wicked
black
magic,
this,
where
error,
so
the
end
hook
extracts
the
hook,
which
is
an
opaque
racket,
object
this,
where
error
extracts
that
opaque
racket
object,
it
uses
the
term
because
it's
saying
this
could
be
any
value.
I
don't
know
what
it
is
and
it's
called
hook.
Then
we
call
this.
This
comma
brings
us
out
of
red
x
out
of
like
logic,
land
and
into
racket
land.
We
call
the
accessor
which
pulls
out
the
field
from
the
struct.
We
call
that
categorized
goal
function.
A
A
Are
gonna
be
just
based
on
categorizations
and
really
we
don't
need
his
atomic
goal
either.
I
don't
know
where
do
we
even
use
that
I
guess
we'll
find
out
now
we
have
to
remove
that
other
stuff
unknowingly,
this
isn't
rust,
so
it's
not
sufficiently
well
typed
for
the
compiler
to
take
us
from
place
to
place
so
we'll
have
to
do
some
searching.
A
Well,
first
of
all,
I'm
going
to
remove
this,
so
this
is
the
list
of
exports
from
the
module,
so
I'm
removing
all
the
functions.
I
deleted
adding
this
one
that
I
added
that
apparently
doesn't
exist
because
I
gave
it
the
wrong
name,
and
now
I'm
gonna
go
into
the
code,
so
this
function
is
calling
is
predicate.
A
That
was
what
we
called
it
right,
yeah
user
predicate,
and
I
think
it's
also
true
for
built-in
predicates
for
better
or
worse,
maybe
we'll
rename
it
to
his
user.
Predicate.
D
A
We
don't
need
two
clauses,
let's
just
keep
those
two
and
see
if
we
need
the
rest.
I
don't
know.
A
D
A
A
So
now
we're
testing
before
we
said,
is
it
a
predicate
and
not
a
built-in
predicate
now
we're
able
to
be
more
selective
with
one
one
statement
or
just
the
thing
we
wanted.
A
This
one,
so
this
checks
for
a
cycle
in
the
this
basically
says,
if
not
for
a
cycle.
This
checks
to
see
if
that
user
predicate
is
defined
in
the
hypotheses-
and
actually
I
think
we
want
is
predicate
here,
because
the
built-in
predicates
are
just
predicates
that
we're
supplying
the
clauses
for
essentially
so
they
can
be
us
just
like
any
other
thing.
They
can
appear
in
the
hypotheses
and
that's
okay
same
here.
This
is
for
co-inductive
cycles.
A
It's
fine
good!
So
far,
so
good.
A
The
main
thing
we
have
to
change
is
here.
So
this
is
the
testing
code
for
lambda.
It's
what
actually
instantiates
that
hook
and
or
there
are
several
cases,
but
this
is
like
the
simplest
one
that
just
tests
the
logic
layer
in
isolation
right
so
right
now
it
has
this.
It
calls.
Logic
is
predicate
which
is
defined
down
here,
and
so
we
need
to
change
this
to.
A
So
these
are
the
three
functions
that
we
just
removed.
We
need
to
get
rid
of
two
of
them
and
redefine
one
of
them
as
logic
categorize
goal.
A
D
A
A
A
A
What
are
the
rules
that
we
have
derived
from
the
user's
declarations?
All
right.
So
if
you
wrote
impulfu
for
bar,
that
translates
into
a
rule
that
says
like
is
is
implemented
of
the
trait
foo
applied
to
the
type
bar
is,
is
correct.
If
the
where
clauses
hold
things
like
that,
and
we
need
a
way
to
get
those
rules
in
to
the
bottom
most
layer
and
in
particular,
there's
an
infinite
set
of
such
rules.
It
turns
out
because
so
you
can't
kind
of
produce
a
total
like
initially,
I
thought
we
would
have.
A
We
take
the
rus
program.
We
would
read
the
declarations
and
convert
it
to
a
set
of
rules
and
then
we'd
hand
the
rules
over
to
the
logic
layer
as
this
like
independent
entity,
but
it
actually
doesn't
work
like
that,
because
there's
an
infinite
set
of
rules.
So
we
could
never
generate
all
the
rules
the
logic
layer
might
need.
So.
A
Instead
we
bundle
up
the
thing
like
the
source
into
the
hook,
where
it's
opaque
to
the
logic
layer,
and
we
give
the
hook
to
the
logic
layer
and
then
the
logic
layer
can
on
demand,
pull
the
rules
that
it
needs
as
it
needs
them,
because
it's
never
going
well.
Hopefully
it
won't
need
all
the
rules
in
that
infinite
set
and
the
reason
there's
an
infinite
set
is
stuff
like
auto
trades
and
I'm
trying
to
remember
what
else.
A
Yeah,
so
that
was
pretty
easy,
so
then
I
think
there's
another
hook
here
yeah,
so
we
also
have
a
place
where
we
test
the
type
layer
in
isolation.
So
we
have.
This
thai
is
predicate.
This
needs
to
become
thai
categorize.
D
A
Well,
the
big
difference
is
actually
type
the
tie.
Layer
does
define
the
grammar
of
predicates,
so
we
can
just.
A
I
see
that's
kind
of
an
interesting
thing.
Well,
it's
okay
and
the
tie
layer
does
not
define
any
built-in
predicates.
It
defines
what
the
set
of
predicates
are,
but
it
doesn't
understand
that
some
of
them
are
built
in
right.
Now,
that's
okay,
don't
think
wind
needs
to.
A
A
A
A
I
deleted
some
of
those
helper
functions
and
I
don't
really
remember
why
I
just
felt
like
it
like.
We
used
to
have
his
atomic
goal
here
and
we
no
longer
do.
I
think,
I'm
going
to
add
it
back
in
because
it's.
A
And
goal
or
no
any,
I
think
I
call
it
or
is
predicate.
A
No,
we
did
have
built
yeah
we,
so
we
replaced
built
in
predicate
with
tie
categories,
cool
that
looks
good.
We
removed
these
two
helpers
added
kite
categories,
goal
from
the
definition
of
logic
hook
or
deckle
hook,
we're
invoking
categorize
goal.
Instead
of
these
more
complex
combinations
of
booleans,
we
added
these
four
classifications
in
defining
the
logic
hook.
A
A
We
remove
these
three
things
from
the
hook.
Good,
we
defined
categorized
goal
in
some
way
to
call
the
hook
function.
We
defined
is
predicate.
A
We
defined
as
relation
and
is
atomic
we
removed
is
built
in
predicate,
but
I
think
we're
no
longer
calling
that
function
because
we're
just
using.
We
only
had
one
caller
and
we
removed
that
too.
A
We
replaced
these
three
things
in
the
defining
the
hook.
With
calling
categories
call,
we
defined
the
logic
layer
version
of
that.
Okay,
we
deleted
this
code.
We
don't
need
to
find
the
type
layer
version.
Okay,
this
is
surely
not
going
to
work,
but
let's
try
I
mean
I.
I
still
don't
expect
this
to
actually
fix
the
bug.
This
is
like
the
refactoring
before
we
can
fix
the
bug,
but
it'll
hopefully
not
die
in
some
new
annoying
way.
A
A
D
A
Okay,
now
we're
getting
the
same
failure
we
got
before
and
we
can
also
test
all
the
things
and
we
won't
have
time
to
do
the
fix,
which
is
too
bad,
but
I
think
it's
actually
relatively
straightforward,
essentially
we're
gonna.
So
what's
the
refactor,
his
predicate
and
friends
to
categorize
school.
A
A
Change
user
predicate
to
user
predicate.
You
know
to
carry
a
proof
co-inductive
along
with
it,
which
we
can
then
match
out
and
pass
in,
and
then
we
have
to
adjust
the
various
functions
that
return
user
predicate
to
return
that:
okay,
thanks
for
attending
and
I'll
post
this
video
after
and
I'll
push
this
branch
somewhere,
but.