Zulip Chat Archive

Stream: lean4

Topic: variables v subtype


view this post on Zulip Kevin Buzzard (Mar 19 2021 at 16:15):

universe u

variable {A : Type u} -- fine

variables {B : Type u} {n : Nat} -- expected '//'
-- error on `u`, presumably subtype notation?

Workaround: use variable not variables when declaring implicit variables.

view this post on Zulip Yakov Pechersky (Mar 19 2021 at 16:17):

I think there is only variable now, and you don't have to declare universe u.

view this post on Zulip Yakov Pechersky (Mar 19 2021 at 16:18):

https://leanprover.github.io/lean4/doc/sections.html?highlight=variable#variables-and-sections
https://leanprover.github.io/lean4/doc/autobound.html

view this post on Zulip Leonardo de Moura (Mar 20 2021 at 17:21):

We have fixed the error message. We now get "expected command" at variables.

view this post on Zulip Kevin Buzzard (Mar 20 2021 at 17:47):

I'm sorry for the noise! I was actually looking at some lean 4 files written by maths undergraduates here and they had used variables but their code was giving me an error with the most recent nightly.

view this post on Zulip Leonardo de Moura (Mar 20 2021 at 17:51):

There is no variables command in Lean 4. We should always use variable.
In my last comment, I was pointing out that the error message is now "sane". If one uses variables or another invalid command, we get "error: command expected" at the right position.


Last updated: May 18 2021 at 22:15 UTC