Zulip Chat Archive

Stream: lean4

Topic: pattern variable issue?


view this post on Zulip Scott Kovach (Jan 12 2021 at 04:11):

myId surprised me:

def myId : List α  List α
| List.nil => List.nil -- i.e. x => x

def constNil : List α  List α
| List.nil => List.nil
| List.cons x y => List.nil

def failing1 : List α  List α
| [] => List.nil

def failing2 : List α  List α
| x => List.nil
| foo.bar => List.nil -- "invalid pattern variable"

I'm guessing that's not intended?

view this post on Zulip Wojciech Nawrocki (Jan 12 2021 at 06:01):

The following also works:

def myId : List α  List α
| foo.bar => foo.bar

Yes, this probably shouldn't compile.

view this post on Zulip Leonardo de Moura (Jan 12 2021 at 14:45):

Pushed a fix: https://github.com/leanprover/lean4/commit/1ebf69e1634a75901bf9f47b7aeec6c8fc624072


Last updated: May 18 2021 at 22:15 UTC