## Stream: new members

### Topic: Rewrite type of term in function definition

#### Alex Keizer (Feb 24 2022 at 15:02):

Is there a way to rewrite the type of a term in a function definition?

I'm getting the following error

type mismatch
foo
has type
motive Foo : Sort u
but is expected to have type
motive Bar : Sort u


But I have a theorem that states

Foo = Bar


So is there a way to use this theorem to resolve the type mismatch?

EDIT: Forgot to mention, I'm working with lean 4

#### Martin Dvořák (Feb 24 2022 at 15:08):

If the theorem is called foobar and you have this error when applying something to your goal, just write:
rw foobar,

#### Martin Dvořák (Feb 24 2022 at 15:11):

Usually, it is better to post your code than to post your error.

#### Reid Barton (Feb 24 2022 at 15:15):

or ideally, post both

#### Alex Keizer (Feb 24 2022 at 15:18):

Yeah, I'm talking about a function definition, rather than a proof.

def List.Nil {α : Type} : List α
:= W.mk (A.Nil) (λ emp => Empty.rec (λ_ => List α) emp)

def List.rec {α : Type} {motive : List α → Sort u}
(mNil : motive List.Nil)
(mCons : (hd : α) → (tl: List α) → motive tl → motive (List.Cons hd tl))
: (t : List α) → motive t
| W.mk (A.Nil) f => mNil  -- <-- mNil is of type motive List.Nil, but motive W.mk Flist_A.Nil f) is expected
| W.mk (A.Cons hd) f => _ -- not important yet


#### Alex Keizer (Feb 24 2022 at 15:21):

So I have a term mNil of type motive List.Nil which I want to return from my function that is declared to return motive W.mk ...,
which seems fine as List.Nil is equal to W.mk ...

#### Alex Keizer (Feb 24 2022 at 15:23):

I could of course change the type of mNil, but the goal is to hide the internal machinery, so that it seems like List.Nil and List.Cons are actual constructors, rather than wrappers around W ...

#### Alex Keizer (Feb 24 2022 at 15:24):

With List.rec the normal high-level recursor that one would expect an inductive type to have

#### Alex Keizer (Feb 24 2022 at 15:43):

Here is a more minimal example:

inductive Foo
| X : (Empty → Nat) → Foo

def bar : Foo
:= Foo.X (λ emp => 1)

theorem foobar (foo : Foo):
foo = bar :=
by
unfold bar
cases foo
apply congrArg
funext x
cases x

def func (motive : Foo → Type) (foo : Foo) (mBar : motive bar) : motive foo
:= mBar -- ERROR


Where the error is again

type mismatch
mBar
has type
motive bar : Type
but is expected to have type
motive foo : Type


#### Reid Barton (Feb 24 2022 at 15:53):

You can use Eq.rec or something, but you're heading down a dark path

#### Alex Keizer (Feb 24 2022 at 16:10):

Thanks for the pointer, I'll see what I can work out

Last updated: Dec 20 2023 at 11:08 UTC