problem with old_structure_cmd

Stream: new members

[David Wärn]

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]

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]

but what caused that error?

[Mario Carneiro]

a bug

[Mario Carneiro]

it's not a whole forest

[David Wärn]

Ah, that will work

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Mario Carneiro]

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]

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]

Which typeclass system is better, Coq or Lean?

[Kevin Buzzard]

seems to be a problem with 3.4.2 as well

[Kevin Buzzard]

meh, restarting VS Code fixed it; no segv

[Kevin Buzzard]

oh no it's back.

[Bryan Gin-ge Chen]

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

[Kevin Buzzard]

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

[Bryan Gin-ge Chen]

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.