►
From YouTube: A Mir Formality Walkthrough 2022-04-20
Description
Implementing the built-in rules for the `Copy` trait in A-Mir-Formality
A
Because
I
figure
it'll
be
useful
and
to
that
end
I
have
this
screen
share
going.
Oh
hello,
everybody
in
the
recording
that
I
just
started
we're
looking
at
mere
formality.
Okay
and
I'm
gonna
send
out,
though
the
link,
if
you
use
oops.
However,
I
do
this.
If
you
use
vs
code,
you
can
join
and
it's
nicer,
maybe
then
seeing
it
in
the
screen.
Sure
if
you
don't
use
vs
code,
you
should
I
don't
know
I
like
it.
A
A
A
C
D
E
A
Yeah
and
the
layers
are
pretty
we'll
see
them
at
play,
but
they're
pretty
important
all
right.
So
let's
do
the
copy
trade.
What
we
did
yesterday
and
I'm
going
to
do
the
same
thing
today
is
we
did
a
type
driven
development
kind
of
thing
where
we
first
wrote
some
tests
and
saw
them
fail
before
we
went
on
and
tried
to
fix
them.
A
A
How
to
logical,
predicates
and
how
to
solve
them
so
so
we're
going
to
make
a
test
for
the
special
rules
of
the
copy,
trait
and
the
main
rule
of
copy
is
that
you
can't
be
copy
unless
all
your
fields
are
copy,
and
so,
let's
see,
we
would
like
to
say
well,
first
of
all,
impul
copy
for
32.
That
should
be
okay.
A
So,
let's
look
at
this
declaration.
The
first
thing
we're
going
to
do
in
this
test
is
we're
going
to
build
up
the
program
that
we're
checking
so
red
x.
Let
that's
basically
a
let
statement
like
in
rest.
It
just
assigns
a
series
of
variables
in
the
case
of
red
x,
every
variable
has
a
name
that
has
every
variable
basically
carries
its
type
because
it
begins
with
the
name
of
the
variable
has
to
first
be
something
from
some
non-terminal
from
the
grammar
right.
A
So
this
is
the
declaration
grammar
which
extends
the
type
grammar,
and
you
have
things
like.
Oh
a
crate
declaration
is
a
series
of
create
declarations
or
sorry,
a
crate
crate.
Decals
is
a
list
of
crate
decal
instances,
a
crate
decal
is
the
name
of
a
crate
and
then
the
contents.
The
contents
is
the
keyword,
crate
and
then
a
series
of
items.
A
I
said
the
keyword
crate,
there's
nothing
about
this.
That
lets.
You
know
it's
a
keyword
in
isolation,
it's
just
that
it's
not
defined
anywhere
else.
That's
what
makes
it
a
keyword.
So
there's
a
lot
of
things
like
that,
which
is
exactly
where
I
said,
there's
a
lot
of
ways
to
write
code
that
isn't
quite
doing
what
you
think
it
is,
if
you
don't
run
it
and
test
it.
A
That's
an
example
where,
like
you
might
think
you
have
a
keyword
or
not
have
a
keyword,
but
nothing
sort
of
explicitly
says
it
one
way
or
the
other.
I've
adopted
the
convention
that
non-terminals
begin
with
capital
letters
and
look
like
rust
type
names,
which
kind
of
at
least
makes
that
relatively
clear.
A
A
I
didn't
do
that,
yet
he
could
that's
a
good
addition
for
another
day
so
who
needs
functions.
You
know
exactly
in
my
my
world
executing
a
secondary
so
right.
So
this
is
a
trait
decal
right.
That's
this
non-terminal
here
and
then
the
underscore
can
you
can
optionally
like
this
is
a
perfectly
valid
variable
name
and
it's
actually
pretty
common.
It
just
says
the
trait
declaration
and
sort
of
works
best.
A
If
there's
only
one
right
a
lot
of
times,
you
only
have
one
thing
of
any
given
type
so,
but
if
you
have
more
than
one
thing
of
a
given
type,
you
want
to
distinguish
them
from
one
another.
So
then
you
put
an
underscore
in
some
distinguishing
name.
So
here
we
have
the
traitdeckle
copy
this
term.
I
actually
don't
think
we
talked
about
this
yesterday
will
but
what's
happening.
Is
that
you're
kind
of
in
in
two
worlds
there's
scheme
world
or
racket?
A
A
Two
or
whatever,
to
add
those
two
numbers
this
would
make
well,
this
would
result
in
three
which
would
then
generate
an
error,
because
three
is
not
a
valid
trait
declaration,
but
but
when
we
say
term,
then
this
this
stuff
gets
interpreted
as
a
red
x
expression
as
a
red
x
term,
rather
move
my
camera
out
of
the
way,
which
means
basically
means
anything
that
you
any
like
random
words
like
trade
will
be
treated
like
keywords
and
and
lists
are
just
like.
This
is
a
three
item
list
and
not
a
call
to
the
function.
A
A
if
you
know
racket-
maybe
you
don't
doesn't
matter
so
we've
got
the
way
we
model
traits,
they
have
first,
the
name.
I
always
put
the
name
to
the
left
just
for
convenience
and
then
the
details-
and
in
this
case
this
is
a
trait.
This
is
the
list
of
generic
parameters,
there's
one.
So
this
is
a
list
of
length
one.
The
one
thing
is
the
pair
of
the
kind
of
the
perimeter
it's
a
type
and
its
name
self
right.
So
we
make
the
the
self
parameter
on
traits
explicit
in
rust,
syntax.
A
A
A
The
next
thing
we're
going
to
add
to
this
test
is
an
implementation.
Implementations
are
a
little
funky
because,
unlike
other
trade,
things
that
go
in
traits,
they
don't
have
names
so
they're,
just
an
impul.
This
list
is
the
list
of
type
parameters
on
the
inpul.
There
are
none.
This
is
the
trait
and
its
parameters
for
which
we
implement.
So
this
is
the
name
of
the
trait.
This
is
a
list
of
parameters
to
the
trait
there's,
exactly
one,
which
is
the
scalar
type
i32.
A
That
is
a
function,
so
that's
the
other
thing
in
red
x.
You
can
make
lists
and
stuff,
but
if
the
first
thing
in
the
list
is
a
function,
that's
in
scope,
then
it
will
be
invoked.
It's
kind
of
like
a
macro.
You
could
think
of
it
like
that.
So
in
this
case
this
is
a
shorthand
that
I
added
because
scalars
are
just
in
in
our
classification
or
just
a
kind
of
rigid
type,
meaning
that
they're
only
equal
to
themselves.
Essentially,
this
is
actually
well.
This
is
how
I'm
currently
modeling
it.
I
think
it.
A
A
This
would
be
the
list
of
where
clauses
there
aren't
any
the
way
that
you
know
what
these
things
would
be
by
the
way.
Let's
see,
I
think
I
can't
just
go
to
definition.
For
this,
though
I
have
to
go.
Is
that
you
look
at
the
grammar
right
so
trait
item
decal
here
it
is
so
this
is
where
the
list
is
right.
There's
a
list
of
kinded
var
ids,
a
kinded
var
id
is
a
pair
of
a
kind
and
a
variety.
So
this
is
a
list
of
those.
That's
the
generics.
D
A
Okay,
the
impul
keyword.
I
think
I
know
what
you're
asking.
If,
if
you
didn't
have
this
keyword,
it
would
be
totally
valid
to
have
like
some
other
kind
of
decal,
to
have
two
non-terminals
that
both
match
to
the
same
set
of
things,
and
when
you
do
the
pattern
matching,
you
couldn't
really
tell
the
difference
between
whether
something
was
originally
a
trait
impuldecal
and
you
just
called
it
a
some
other
kind
of
decal
or
not
that's,
sort
of
like
a
subtyping.
A
E
E
But
we
don't
and
then,
since
I
suspect,
that
this
kind
of
pattern
that
we're
doing
right
now
is
something
that
people
will
want
to
experiment
with.
Can
we
go
back
to
that
red
x?
Let
statement
and
just
can
you
kind
of
just
show
us
what
the
like
scope
of
the
like
parentheses
are
like,
because
let
means
we're
kind
of
like
binding
some
variables.
A
Yeah,
so
right,
so
let
the
way
the
structure
of
a
let
in
scheme
and
in
red
x
and
then
racket
is
first,
you
have
a
list
delineated
by
a
parenthesis.
Actually,
racket
lets
you
use,
you
don't
have
to
use,
parentheses
could
use
like
brackets,
but
anyway,
you'll
see.
I
do
that
in
some
places
it
has.
Basically,
it
looks
like
this.
We
made
it
more
abstractly.
A
A
red
xlet
is
a
list
of
like
variable
names
and
then
variable
value
pairs,
and
then
a
body
and
this
body
will
be
evaluated
with
each
of
these
variables
in
scope
and
this
star,
there's
both
with
and
without
the
star.
The
star
means
that
each
variable
is
available
in
scope
immediately
so
like.
If
you
have
variable
name
two,
this
could
reference
variable
name
if
it
wanted
to.
A
A
A
A
good
equivalent
to
this
in
rust,
I
guess
we
should
probably
that
accesses
various
bits
of
functionality.
I
guess
you
could
kind
of
like
cargo.
One
of
them
is
that
it
can
run
tests
and
you
can
just
kind
of
give
it
a
path
I
like
to
do.
J14
and
dash
t
j14
means
run
using
14
threads.
That's
how
many
cores
I
have
the
path.
A
So
if
I
run
source,
I'm
going
to
run
all
the
tests
that
are
found
in
the
source
directory
and
it's
going
to
take
a
little
while
because
it's
not
the
fastest
thing
ever,
but
that's
okay,
and
we
will
see
that
this
test
fails.
I
hope,
but
what
we'll
also
see
is
that
the
error
message
you
get
when
using
rako
or
the
back
trace
you
get
is
not
that
great.
A
It
may
not
be
too
bad
in
this
particular
instance
yeah.
So
you
can
see
we
got
a
failure
here.
It
said
that
this
term
that
we
wrote
did
not
match
the
pattern
we
expected-
and
this
is
a
good
example
of
why
the
back
traces
can
sometimes
be
not
that
great
if
you're
using
rako.
You
know
none
of
this
is
my
code
right.
This
is
like
error.racket.
A
This
is
sort
of
talking
about
my
code,
but
it's
not
the
file
name
of
my
code,
and
this
is
some
other
thing
so
what's
happening.
Is
that
there's
like
layers
and
layers
of
macros
and
if
you
just
run
in
racco
to
make
things
go
faster?
They
don't
save
all
the
expansion
back
traces,
so
you're
only
seeing
the
actual
macro
definitions,
which
are
not
that
interesting,
because
I
don't
you
know,
you're
not
familiar
with
them.
A
Oh
by
the
way,
the
dash
t
shows
a
table
and
it
just
kind
of
shows
you
like:
where
was
the
actual
errors?
Oh,
there
was
one
error
in
this
file.
That's
why
I
like
it.
So
what
you
can
do,
there's
this
wacky
command,
that
we
have
to
record
and
probably
make
a
shell
script
or
something
so
we
don't
have
to
keep
typing
all
the
time.
A
A
A
A
I
could
have
there's
no
reason
I
have
to
make
these
intermediate
variables.
You
could
just
inline
everything
directly
in
here.
If
you
wanted
the
reason
I
don't
do,
that
usually
is
because
this
way
I'm
like,
if
you
make
a
mistake
somewhere
in
there,
we're
just
going
to
find
out.
Oh,
this
is
not
a
valid
crate,
and
that's
all
that's
not
that
helpful.
This
way
I
can
localize
my
my
mistake
to
the
exact
location,
okay
and
then
what
this
does.
A
A
A
Well,
it's
done
that
lazily
actually,
but
right,
it's
going
to
make
an
environment,
so
this
is
a
shorthand
for
saying
that,
there's
a
single
crate
and
we're
going
to
make
environment
from
that
there's
a
longer
form
that
takes
a
full
list
of
dependencies.
If
you
wanted
to
have
more
than
one
crate,
which
would
be
important
say
for
the
coherence
rules
to
be
able
to
separate
out,
like
which
crate
is
the
impul
in
and
and
so
forth.
A
So
the
way
this
actually
works,
I
won't
go
too
much
into
that,
but
it
uses
this
just
creates
an
environment
that
carries
a
little
hook.
That
has
some
lambda
functions
that
we
can
call
later
to
do
things
like
say
give
me
all
the
clauses
that
might
prove
this
predicate
and
so
on.
But
now
we
have
this
environment,
and
now
we
can
actually
write
our
test,
and
here
we
want
test
can
prove
that's
going
to
that's
a
test
that
says
we
should
be
able
to
prove
given
this
environment
that
this
crate
is
well
formed.
A
So
the
okay
goal
or
is
okay,
the
okay
goal
basically
says
all
the
type
checks
and
checks
were
successful.
You
could
generate
code
from
this
crate
if
you
wanted
to
so
right
now.
That
means
the
well
form
in
this
checks,
but
if
or
when
we
add
a
type
checker
and
stuff,
that
would
mean
that
the
functions
also
type
check
and
so
on.
A
A
A
That's
usually
like
if
you
see
that
something
doesn't
match
the
pattern,
at
least
for
me,
it's
always
one
of
two
things.
Either
I
have
a
typo
somewhere,
in
which
case
I
see
some
random
name
like
that.
That
looks
out
of
place,
or
I
don't
have
enough
parentheses,
and
that
usually
happens
when
it's
like
a
list
of
lists
like
this
is
a
list
of
length
one,
but
it
sort
of
looks
like
a
list
anyway.
A
So,
what's
that
oh,
what's
trace,
what's
trace
doing
right?
That's
a
good
question
traced
is
a
trick.
Past
yay,
no
wait!
No
output
equals
good
traced
is
a
macro
which
I
wrote.
That
brings
the
s
that
uses
this
red
x
function
to
say:
here's
a
list
of
meta
functions,
meaning
functions
in
the
not
functions
in
your
program
with
functions
in
your
type
checker
that
we
want
to
trace
as
they
execute.
So
it's
for
debugging.
A
So,
for
example,
we
could
go
into.
Let
me
just
show
you
this.
This
crate.
Okay
goal
is
itself
a
function
right.
We
could
say
I'd
like
to
see
every
time
you
call
this
function,
what
are
its
inputs
and
outputs
because
something's
not
working
right,
so
we
could
add,
create
ok
goal
into
that
list
and
run
the
code.
A
A
So
right,
so
here
you
see,
this
is
the
function.
Call
this
you
know,
tells
you
it's
coming
in
and
then
coming
out.
This
is
the
goal
we
actually
had
to
prove
in
order
to
show
that
this
crate
was
well
formed,
and
this
goal
is
computed
by
essentially
looking
at
each
item
in
turn
and
figuring
out
what
would
be
its
correctness
criteria.
So,
in
the
case
of
the
the
copy
trait
itself,
this
is
the
rule.
A
A
A
A
No
generic
parameters,
it
has
no,
where
clauses
and
what
this
is.
This
is
a
list
of
variants,
so
in
an
enum
there
would
be
multiple
variants
potentially,
but
in
a
struct
there's
always
exactly
one.
I
have
been
calling
it
after
the
struct
itself.
Every
variant
has
a
name,
so
this
would
be
like
sum,
and
none
for
option
right,
but
we
don't
know
we
can
establish
a
different
convention
and
inside
the
variant
there's
a
list
of
fields,
but
we
don't
have
any
fields.
So
this
should
be
all
set.
A
A
So
that's
a
thai
rigid
food,
the
what's
this
thai
rigid,
that's
the
kind
of
type,
that's
the
name
of
the
adt,
and
this
is
the
list
of
type
parameters.
There
are
none,
so
this
is
the
one
field
we
have
in
this
list.
My
usual
formatting
convention
is
if
this
is
a
list
that
it
would
make
sense
to
add
more
things
into
like
it's
an
open-ended
list,
then
I
put
the
closing
parenthesis
on
the
final
line.
A
A
D
A
So
right,
our
test
failed
this.
That
gold
test
cannot
prove
just
it's
not
some
built-in
thing.
It's
actually
a
macro
that
I
added,
which
so
defines
syntax
rules
like
macro
rules.
Right,
it
says,
cannot
prove
for
an
environment,
a
goal
and
all
it
does.
Is
it
tests
equal
to
false
this
red
x
thing
that
says?
Can
I
prove
this
judgment?
So
that's
why
you
see
actual
true,
because
it
was
actually
successful
and
expected
false.
A
Okay
cool,
so
we
got
our
test
doesn't
work.
How
do
we
fix
it?
Well,
what
we
want
to
do
is
go
into
the
rule.
Go
into
this
function,
create
ok
goal
and
change.
The
ok
goal
for
the
trait
to
reflect
the
extra
conditions
that
the
copy
trait
has
right,
and
so
we've
set
it
up.
There's
two
parts:
basically,
what
you
have
this
is
the
list
remember
create
decals.
This
is
all
the
definitions
of
all
the
crates,
and
then
this
is
the
specific
crate
that
we're
compiling
right
now,
it's
kind
of
the
local
crate.
A
A
Yeah
there
we
go
so
this
weird
notation
means
well
racket.
People
like
their
leading
leading,
I
shouldn't
be
so
judgmental
this
racket,
notation
of
a
hash
sign,
means
funky
stuff
and
in
this
case
it's
a
precondition.
So
this
is
a
red
x
thing
that
must
evaluate
to
true
in
question.
Mark
is
actually
a
function.
I.
B
A
Or
no,
no
one,
so
we
should
be
able
to
go
to
definition.
Now,
it's
very
simple
function
in
is
true,
if
this
first
term,
if
there,
if
there
is
some
term
in
this
list,
so
it
takes
it
takes
one,
a
term
is
anything
right
term
could
be
any
it's
a
grammar
for
anything
one
thing
and
a
list
of
things.
If
that
first
thing,
if
there
is
something
in
the
list
that
is
alpha,
equivalent,
meaning
can
have
variables
that
are
bound
can
be
renamed
to
term
zero,
then
it's
true.
Otherwise
it's
false.
A
A
Okay.
So
anyway,
that
little
aside
aside,
we
are
now
going
through
we.
This
is
the
current
crate
that
we're
compiling.
This
is
the
list
of
all
the
items
in
the
crate,
this
dot,
dot,
dot
means
match
more
than
one
thing,
and
so
what
we're
going
to
do
is
we're
we're
going
to
map
over
these
items
and
produce
two
sets
of
goals.
A
The
first
one
is
the
kind
of
standard
goals
that
tell
you
that
a
given
item
is
okay,
so
these
will
be
for
any
like
for
any
structure
any
trait.
These
are
the
base
conditions
that
have
to
be
met,
and
then
we
have
this
function.
Laying
item,
ok,
goals
that
says:
are
there
some
extra
rules
built
into
the
language
that
are
specific
to
this
particular
trait?
You
know,
and
not
shared
by
all
traits
or
specific,
this
particular
struct
or
whatever?
A
Yeah
we
made
it
for
drop,
but
we're
going
to
use
it
again
and
the
thing
about
the
laying
item.
Okay
goals,
if
you
go
to
that
definition,
is
that
for
a
given
crate
item,
it
returns
a
list
of
goals
which
may
be
the
empty
list
and
the
reason
we
do
that
is
for
things
that
are
not
laying
items.
We
just
return
the
empty
list
for
things
that
are
laying
items.
We
could
return
multiple
goals
or
you
know
whatever
we
wanted.
A
The
reason
that's
relevant
is
here
we're
mapping
this
function
over.
We're
saying
do
that
for
every
crate
item,
so
we're
going
to
get
a
list
of
lists
right,
this
first
dot,
dot,
dot,
means
for
each
crate
item
and
then
inside
of
that
there'll
be
a
list
of
goals.
That's
what
the
second
dot
dot
is
telling
us,
and
so
then
we
can
use
two
dot
dot
dots
here
to
flat
map.
This
is
basically
concatenating.
A
B
A
Okay,
so
right
so
here
we
have
this.
Laying
item.
Ok,
goals
function.
This
is
the
rule
for
drop,
we're
going
to
do
a
similar
rule
for
copy.
So
I'm
going
to
copy
this.
No,
I
won't
copy
it
because
it'll
be
clearer.
If
I
start
it
over,
I
think
you
can
see
I
this
is
like
the
main
place
I
use
brackets.
I
don't
know
why
just
the
convention
I
stole
from
them,
I
guess
inside
a
meta
function.
I
usually
use
brackets
for
each
possible
case.
A
A
Why
did
that
not
work?
Sometimes
there's
like
a
race
condition
in
this.
I've
noticed
before
in
the
vs
code
extension
that
when
you
hit
command
copy,
it
takes
a
little
while
to
actually
do
the
copy.
I
don't
know
why,
and
so
I'm
too
fast
for
it
or
something-
and
I
end
up
pasting
random
stuff.
I
think
it
has
to
do
maybe
with
running
over
ssh
so
right.
So
this
is
the
name
of
the
function
and
then
these
are
patterns
to
match
against
each
parameter.
A
A
This
is
the
list
of
parameters.
Copy
only
has
one,
so
we
just
need
one,
and
we
know
it's
a
type.
Ordinarily,
you
might
have
like
a
lifetime,
or
you
know
whatever.
This
was
a
generic
trait.
This
was
partially
q.
There
would
be
two
types
in
here
and
then
this
is
the
list
of
where
clauses
on
the
impul.
This
is
the
list
of
items
in
the
impul
copy,
doesn't
have
any
so
we
could
just
put
an
empty
list
there.
A
A
A
D
A
Which
is
this
comes
from
the
struct,
the
exit,
basically
we're
going
to
match
against
the
struct
here,
so
we're
going
to
say
that
there's
some
given
some
type
parameters,
t
for
the
struct,
where
this
type
equals
that
type,
so
foo
of
t
is
full
of?
U
then,
and
now
we're
going
to
add
in
for
each
field
in
the
struct
back
of
t
that
better
be
copy,
that's
the
condition
we
want
to
be
met.
A
F
A
A
Okay,
so
now
we
want
to
generate
this,
we
have
10
minutes.
I
think
we
can
do
it,
but
let
me
skip
this
we're
going
to
need
some
of
this
stuff.
Oh,
I
didn't
finish
telling
you
the
structure
of
this
stuff.
So
this
is
the
thing.
This
is
the
pattern
we're
going
to
match
against
and
then
this
is
the
return
value.
A
Usually
I
just
put
xxx
there
or
something
because
there's
this
weird
evaluation
order.
Where
you
know
it
starts
by
matching
the
pattern,
then
it
executes
all
the
where's
and
where
errors
I'll
get
to
in
a
second
and
then
it
generates
the
return
button.
So
I
like
to
put
something
there,
so
I
don't
forget
and
then
go
write
the
code.
A
Correct
there's
a
difference
between
the
drop
rule
and
this
rule.
That
drop
is
trying
to
say
has
this
is
saying
something
is
true
for
every
instance
of
the
struct,
but
in
this
rule
we
don't
need
it
to
be
true
for
every
instance
of
foo.
We
only
need
to
be
true
for
those
types
of
food
that
are
copied
so
we're
actually
quantifying
over
the
impul.
C
C
A
Wouldn't
it
be
shadowed
or
would
there
be
a
problem?
The
answer
is
yes,
there
would
be
a
problem
except
that
red
x,
we've
told
red
x
about
the
binding
and
it's
gonna
do
the
renaming
it
behind
our
back,
so
that
there's
never
any
shadowing.
So
we
don't
have
to
worry
about
that
which
is
kind
of
cool
so
right.
So
what
are
we
doing?
So
I
matched
against
the
impul.
A
What
I'm
doing
here
is
just
destructuring,
some
of
these
non-terminals
into
their
pieces
like
here
I
said
we
have
some
type
well.
What
I
want
to
say
is
if
that
type
is
an
adt
right,
so
I'm
putting
the
where,
where
means,
if
this
is
not
true,
then
move
to
the
next
case
right.
So
if
this
destructuring,
this
pattern
match,
fails
we're
going
to
go
and
execute
this
next
case
other
times
actually
most
of
the
time.
A
A
It's
a
pretty
important
distinction
for
debugging,
so
it's
worth
making
it
consistently.
Otherwise,
really
weird
stuff
happens
where
it
just
goes
running
off
into
matches.
You
don't
expect
so
right,
so
we're
gonna
say
the
thing
is
this:
there
could
be
many
kinds
of
copy
impulse
that
are
not
of
adt's
and
those
might
be
okay.
You
may
have
some
more
rules
down
there,
but
for
now
we're
only
concerned
about
ats,
so
we're
doing
aware
of
a
fallible
where
and
then
this
function.
A
What
this
does
is.
It
goes
off
and
fetches
the
definition
given
the
full
set
of
items,
all
the
crates
fetches,
the
definition
for
this
name.
So
I
assume
everything
has
distinct
names,
make
my
life
easier
right
and
then
this
pattern
is
matched
against
the
definition,
the
actually,
what
I
should
be
writing
here
hold
on
a
second
grammar.
A
A
So
there's
a
subtle
point
here,
which
is
that,
although
I
wrote
adt
id
indicating
this
is
the
name
of
an
adt
actually
from
red
x's
perspective,
all
well,
it's
not
in
this
list,
but
there's
another
list
somewhere
else.
That's
similar,
all
ids
are
are
some
kind
of
variable
name
like
it
doesn't
really
know
that
just
means
string.
A
In
short,
it
means
a
string
that
doesn't
show
up
anywhere
else
in
the
grammar.
So
maybe
this
isn't
really
the
name
of
an
adt.
Maybe
it's
the
name
of
a
trait
or
something.
So
that's
why
I
make
this
next
thing.
Fallible
too,
because
once
I
found
the
definition
for
adt
id
and
it
indeed
matches
the
form
of
an
adt.
I
know
it
really
is
an
adt,
but
it's
I
find
it
pretty
useful
to
distinguish.
You
know
what
I
think
it
is,
but
that's
an
important
thing
to
keep
in
mind
I've
occasionally
written
code.
A
That
was
bogus
for
that
reason.
So
right
so
now
we
have
an
adt.
This
is
the
definition
of
the
struct,
in
other
words,
here's
the
generics.
Here's
the!
Where
clauses
we
don't
actually
care
about
the
where
clauses
from
what
I
can
tell
so
I'm
going
to
get
rid
of
them,
and
now
we
have
to
generate.
I
don't
think
we
need
to
do
anything
else,
let's
find
out
so
we're
going
to
generate
this
return
value.
A
B
A
Oh
no
yeah!
Okay,
before
I
go
further,
there's
a
subtle
point
here,
where
clauses
I
use
that
to
refer
to
the
rust,
syntax
and
actually
yeah.
I
use
that
to
refer
to
the
rest
syntax,
but
what
we're
doing
now
is
generating
a
logical,
predicate
and
those
are
richer.
There
are
more
kinds
of
predicates
and
they
don't
map
one
to
one
to
where
clauses
like
where
clauses
can
be
mapped
predicates,
but
not
back,
not
vice
versa,
and
so
what
we
actually
want
is
not.
A
A
Yeah
we're
going
to
get
to
that.
Oh
well!
No,
we
won't,
I
guess
but
yeah
in
the
case
of
in
the
case
of
drop,
we
used
some
of
the,
where
clauses
were
things
that
we
got
to
assume
those
we
convert
with
the
hypotheses
function
and
others
were
things
we
wanted
to
prove.
So
in
that
case
we
use
the
goal
function.
A
A
It
does
which
I
think
we
should
change
it.
I
guess
right
now
it
partially
overlaps,
not
always
in
particular
outlives
relations
are
different.
I
think
we
should
change
it
so
that,
where
clauses
look
more
like
rust
like,
I
would
like
you
to
not
have
to
write
implemented
in
the
rust
like
syntax
and
get
translated,
and
there
would
be
two
advantages.
One,
the
syntax
would
look
more
like
rust
and
two.
A
B
A
We
need
this
code
hold
on.
I
forgot
about
this
okay,
so
what's
happening
here.
This
is
a
list
of
pairs.
We
only
want.
We
don't
need
the
kinds.
We
only
want
the
names
of
the
variables
so
we're
going
to
just
pattern
match
against
the
list
of
pairs
and
pull
out
the
second
half.
This
is
the
type
like
foo
of
t.
A
We
can
put
it
in
there
and
then
we
also
want
to
say:
oh
we're
not
quite
there.
I'm
gonna
have
to
go
because
I
have
this
other
meeting,
but
what
we
should
add.
I
could
push
this
somewhere
if
someone
wants
to
take
their
take
a
stab
at
it.
But
what
we
should
add
now
is
we
need
to
here's
the
adt
variants.