Zulip Chat Archive

Stream: new members

Topic: problem with old_structure_cmd


view this post on Zulip David Wärn (Apr 22 2020 at 07:33):

set_option old_structure_cmd true
class foo (α : Type) extends partial_order α, densely_ordered α
type mismatch at application
  @partial_order.to_preorder α le_antisymm
term
  le_antisymm
has type
   (a b : α), a  b  b  a  a = b
but is expected to have type
  partial_order α

What does this error mean? It seems to have to do with densely_ordered assuming preorder

view this post on Zulip Mario Carneiro (Apr 22 2020 at 07:57):

I suggest setting it up like this:

import order.basic
set_option old_structure_cmd true
class foo (α : Type) extends partial_order α :=
(dense : densely_ordered α)

instance foo.densely_ordered {α} [foo α] : densely_ordered α := foo.dense _

view this post on Zulip Kenny Lau (Apr 22 2020 at 07:58):

but what caused that error?

view this post on Zulip Mario Carneiro (Apr 22 2020 at 07:58):

a bug

view this post on Zulip Mario Carneiro (Apr 22 2020 at 07:59):

it's not a whole forest

view this post on Zulip David Wärn (Apr 22 2020 at 08:02):

Ah, that will work

view this post on Zulip Kevin Buzzard (Apr 22 2020 at 08:15):

If it's a bug you should open an issue, right?

view this post on Zulip Kevin Buzzard (Apr 22 2020 at 09:42):

What is going on here? I've never seen that before. import order.basic at the top of David's code

view this post on Zulip Mario Carneiro (Apr 22 2020 at 10:03):

This is the first time I have seen someone try to have a regular structure extend a structure and another structure parameterized over the first. (That is, densely_ordered A takes a parameter of type partial_order A.) I think the extends mechanism doesn't know how to pass the parameters properly in this case.

view this post on Zulip Kevin Buzzard (Apr 22 2020 at 10:10):

set_option old_structure_cmd true

class A (α : Type) :=
(a : true)

class B (α : Type) extends A α :=
(b : true)

class C (α : Type) [A α] :=
(c : true)

class D (α : Type) extends B α, C α.

I get failed to add declaration to environment, it contains local constants and then after a few seconds a SIGSEGV

view this post on Zulip Kenny Lau (Apr 22 2020 at 10:13):

Which typeclass system is better, Coq or Lean?

view this post on Zulip Kevin Buzzard (Apr 22 2020 at 10:15):

seems to be a problem with 3.4.2 as well

view this post on Zulip Kevin Buzzard (Apr 22 2020 at 10:22):

meh, restarting VS Code fixed it; no segv

view this post on Zulip Kevin Buzzard (Apr 22 2020 at 10:24):

oh no it's back.

view this post on Zulip Bryan Gin-ge Chen (Apr 22 2020 at 15:31):

Since there's a period at the end of the file that crashes, I'm pretty sure this is lean#85.

view this post on Zulip Kevin Buzzard (Apr 22 2020 at 15:36):

I was trying to understand the partial order error and have run into something else

view this post on Zulip Bryan Gin-ge Chen (Apr 22 2020 at 15:40):

You can work around it by adding any code or comment after the period. It'd be good to fix the crash, but I haven't been able to summon the energy to dig into that part of the scanner.


Last updated: May 17 2021 at 23:14 UTC