Error for List \a exercises?

Stream: new members

[Leona]

I am working through "Dependent Types in Lean" and having some technical trouble with the midchapter exercises for List types. When I try to copy the example code into VS Code, it returns errors on all the theorems, even when marked as "sorry".

For example, the following is marked as an error, saying it expects type "sorry" for rfl:

theorem nil_append (as : List α) : append nil as = as :=
 rfl

What's up with this?

[Ruben Van de Velde]

I get

Function expected at
  append
but this term has type
  ?m.2

Note: Expected a function because this term is being applied to the argument
  nil

which indicates you forgot imports in your code

[Aaron Liu]

Can you link to "Dependent Type in Lean"?

[Leona]

https://leanprover.github.io/theorem_proving_in_lean4/Inductive-Types/#other-recursive-data-types

[Aaron Liu]

oh it's #tpil

[Leona]

Sorry, "Theorem Proving in Lean"

[Leona]

yes, my bad

[Aaron Liu]

I clicked on "show hidden lines" and it gave me

namespace Hidden
inductive List (α : Type u) where
| nil  : List α
| cons : α → List α → List α
namespace List
def append (as bs : List α) : List α :=
 match as with
 | nil       => bs
 | cons a as => cons a (append as bs)
theorem nil_append (as : List α) : append nil as = as :=
 rfl
theorem cons_append (a : α) (as bs : List α)
                    : append (cons a as) bs = cons a (append as bs) :=
 rfl
theorem append_nil (as : List α) :
    append as nil = as :=
  sorry

theorem append_assoc (as bs cs : List α) :
    append (append as bs) cs = append as (append bs cs) :=
  sorry
end List
end Hidden

[Leona]

yes i copied that into my ide, still got the errors

[Aaron Liu]

the "copy" gives me

namespace Hidden
inductive List (α : Type u) where
| nil  : List α
| cons : α → List α → List α
namespace List
def append (as bs : List α) : List α :=
 match as with
 | nil       => bs
 | cons a as => cons a (append as bs)
theorem nil_append (as : List α) : append nil as = as :=
 rfl
theorem cons_append (a : α) (as bs : List α)
                    : append (cons a as) bs = cons a (append as bs) :=
 rfl
namespace Hidden
inductive List (α : Type u) where
| nil  : List α
| cons : α → List α → List α
namespace List
def append (as bs : List α) : List α :=
 match as with
 | nil       => bs
 | cons a as => cons a (append as bs)
theorem nil_append (as : List α) : append nil as = as :=
 rfl
theorem cons_append (a : α) (as bs : List α)
                    : append (cons a as) bs = cons a (append as bs) :=
 rfl
theorem append_nil (as : List α) :
    append as nil = as :=
  sorry

theorem append_assoc (as bs cs : List α) :
    append (append as bs) cs = append as (append bs cs) :=
  sorry
end List
end Hidden

[Aaron Liu]

it seems there's a problem with "copy"

[Leona]

ahh, hmm

strange!

[Leona]

Aaron Liu said:

I clicked on "show hidden lines" and it gave me

namespace Hidden
inductive List (α : Type u) where
| nil  : List α
| cons : α → List α → List α
namespace List
def append (as bs : List α) : List α :=
 match as with
 | nil       => bs
 | cons a as => cons a (append as bs)
theorem nil_append (as : List α) : append nil as = as :=
 rfl
theorem cons_append (a : α) (as bs : List α)
                    : append (cons a as) bs = cons a (append as bs) :=
 rfl
theorem append_nil (as : List α) :
    append as nil = as :=
  sorry

theorem append_assoc (as bs cs : List α) :
    append (append as bs) cs = append as (append bs cs) :=
  sorry
end List
end Hidden

even copying this still throws up the errors!

[Aaron Liu]

It works fine in the web editor

[Aaron Liu]

what's the error you are experiencing?

[Leona]

Application type mismatch: In the application
append nil
the argument
nil
has type
List ?m.15230 : Type ?u.15229
but is expected to have type
Type : Type 1

[Aaron Liu]

what's your definition of append?

[Leona]

ahhh, just supplied the argument \a before nil and it checks!

[Leona]

The exercise had the type for append wrong