## Stream: new members

### Topic: problem with old_structure_cmd

#### 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

#### 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 _


#### Kenny Lau (Apr 22 2020 at 07:58):

but what caused that error?

a bug

#### Mario Carneiro (Apr 22 2020 at 07:59):

it's not a whole forest

#### David Wärn (Apr 22 2020 at 08:02):

Ah, that will work

#### Kevin Buzzard (Apr 22 2020 at 08:15):

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

#### 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

#### 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.

#### 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

#### Kenny Lau (Apr 22 2020 at 10:13):

Which typeclass system is better, Coq or Lean?

#### Kevin Buzzard (Apr 22 2020 at 10:15):

seems to be a problem with 3.4.2 as well

#### Kevin Buzzard (Apr 22 2020 at 10:22):

meh, restarting VS Code fixed it; no segv

oh no it's back.

#### 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.

#### Kevin Buzzard (Apr 22 2020 at 15:36):

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

#### 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