Zulip Chat Archive

Stream: lean4

Topic: dumb questions


Chris Lovett (May 28 2022 at 02:02):

Can someone help me get a Tree walk function working? I'm trying to copy how the Json render function works but I'm getting a strange error:

inductive Tree (β : Type v) where
 | leaf
 | node (left : Tree β) (key : Nat) (value : β) (right : Tree β)
deriving Repr

def walk  : Tree β  String
  | leaf => "leaf"
  | node l k v r => "node: " ++ (toString k) ++ (v) ++ "\n" ++ (walk l) ++ "\n" ++ (walk r)

error: invalid pattern, constructor or constant marked with '[matchPattern]' expected?

Mario Carneiro (May 28 2022 at 02:04):

leaf and node aren't in scope

Mario Carneiro (May 28 2022 at 02:05):

You can fix this with either open Tree or def Tree.walk or use .leaf and .node in the patterns

Chris Lovett (May 28 2022 at 02:05):

Doh! thanks, not the best error message... :-)

Henrik Böving (May 28 2022 at 12:22):

The reason its giving you this error message is that it is interpreting node as a named wildcard pattern (which is in principle correct) but now you're also giving the thing arguments as if it was a function (l k v r) which doesnt make sense since the wildcard pattern can of course not receive arguments.

It also did the same with leaf but since leaf doesn't have arguments it goes through as a normal named wildcard.

You can also recognize the difference between a match pattern being interpreted as a wildcard and as a real constructor based on it's highlighting:

As wildcard:
image.png

As constructor:
image.png

Malcolm Langfield (May 29 2022 at 20:59):

I've just tried to run this for kicks, and I've gotten an error message I don't understand (scroll to the right if you can't see it):

  inductive Tree (β : Type v) where
   | leaf
   | node (left : Tree β) (key : Nat) (value : β) (right : Tree β)
  deriving Repr

  def walk  : Tree β  String
    | .leaf => "leaf"
    | .node l k v r => "node: " ++ (toString k) ++ (v) ++ "\n" ++ (walk l) ++ "\n" ++ (walk r)      failed to synthesize instance    HAppend String β ?m.5860

I see in the Lean 4 source that HAppend is responsible for the ++notation, and is a typeclass taking three arguments, and the first two look all right:

class HAppend (α : Type u) (β : Type v) (γ : outParam (Type w)) where
   hAppend : α  β  γ      (kernel) unknown constant 'Eq.ndrec'

So I assume it's unhappy about whatever it's getting for γ. But I don't really understand how this class is being instantiated when you use this notation.

Sebastian Ullrich (May 29 2022 at 21:11):

What the error message is trying to say is that Lean doesn't know how to append a String ("node: " ++ (toString k)) and a β ((v))

Henrik Böving (May 29 2022 at 21:12):

First things first there is not actually a reason to use the append notation here, we might as well use s! notation like this:

 def walk  : Tree β  String
   | .leaf => "leaf"
   | .node l k v r => s!"node: {k} {v}\n{walk l}\n{walk r}"

this does however still throw an error (and as we will see this is also the reason why the append notation fails)

failed to synthesize instance
  ToString β

so let's add that instance to our arguments:

 def walk [ToString β] : Tree β  String
   | .leaf => "leaf"
   | .node l k v r => s!"node: {k} {v}\n{walk l}\n{walk r}"

Now everything works.

So what's happening above is that everything comes down to:

 def walk  : Tree β  String
   | .leaf => "leaf"
   | .node l k v r => (toString k) ++ (v)

this not working out properly, it produces the same error message:

failed to synthesize instance
  HAppend String β ?m.1520

If we were to use toString on vand add the corresponding instance parameter everything would work just fine.

Henrik Böving (May 29 2022 at 21:12):

And i spent 5 min writing this essay /o\

Sebastian Ullrich (May 29 2022 at 21:13):

The essay is definitely more helpful :)

Malcolm Langfield (May 29 2022 at 21:48):

@Sebastian Ullrich @Henrik Böving Thanks for the quick explanations! I definitely like how the error message is a bit more clear (imo) when you use the string interpolation. So is it correct to read the square bracket/typeclass resolution notation as "β must implement ToString"? And for fixed β, we would achieve this by writing something of the form instance ToString β where ...?

Henrik Böving (May 29 2022 at 21:51):

You are missing a colon: instance optionalName : ToString β where but yes in principle you are right.

Chris Lovett (May 30 2022 at 22:20):

Another dumb question, I'm trying to parse XML and it took me forever to figure out that the import statement and the open statement have to be different and I'm wondering if there are any debug things that tell me what symbols are in scope when I use the open statement so I can debug this sort of thing:

import Lean.Data.Xml
open Lean.Xml
#eval parse "<root/>"

I also missed this magic combination a couple times until I realized that the Lean LSP was just being slow, seems when you import something it takes a few seconds to catch up? It might be handy to change the InfoView (or popup tips) to "busy" in this case so I know it's not done yet...

Henrik Böving (May 30 2022 at 22:56):

Regarding the first: I usually do #check Lean.Xml. and check out the auto completion at that point

Regarding the second thing, if I import something heavy and it takes a while I can see my emacs indicating that in the left side bar by colouring it orange
image.png
as the compiler progresses during the file it begins removing the orange bar from the lines that it already checked

Chris Lovett (May 31 2022 at 00:02):

Thanks, I have another one, what does the $ operator do?

partial def manyCore (p : Parsec α) (acc : Array α) : Parsec $ Array α :=
  (do manyCore p (acc.push $ p))
  <|> pure acc

I think it's implemented here, but I couldn't figure it out from there...

def macroArg       := termParser maxPrec
def macroDollarArg := leading_parser "$" >> termParser 10
def macroLastArg   := macroDollarArg <|> macroArg

As the only place this is referenced is in BuildinNotation under elabStateRefT...?

Hanting Zhang (May 31 2022 at 00:05):

Parsec $ Array α is equivalent to Parsec (Array α). It doesn't do anything, but it binds with very low precedence so that you can avoid stacking parentheses

Hanting Zhang (May 31 2022 at 00:06):

So something like f (g (h x y)) can be written as f $ g $ h x y

Chris Lovett (May 31 2022 at 00:46):

Awesome thanks, totally wouldn't have figured that out from the code. A comment to that effect in the code would have been nice. Better yet, a comment that would then also popup when I hover my mouse over the $ symbol...

Malcolm Langfield (May 31 2022 at 11:20):

There is some documentation here: https://leanprover.github.io/lean4/doc/functions.html

For users familiar with the Haskell programming language, Lean also supports the notation f $ a for the backward pipeline f <| a.

The forward pipeline |> operator takes a function and an argument and return a value. In contrast, the backward pipeline <| operator takes an argument and a function and returns a value. These operators are useful for minimizing the number of parentheses.

Example from the manual:

def add1 x := x + 1
def times2 x := x * 2

#eval times2 (add1 100)
#eval 100 |> add1 |> times2
#eval times2 <| add1 <| 100

Malcolm Langfield (May 31 2022 at 11:22):

Admittedly it's not exactly easy to find if you're specifically looking for a definition of the $ operator, and don't already know your way around the manual.

Remi (May 31 2022 at 14:41):

How can I write this function?

def TType.eq : TType  TType  Option (t₁ = t₂)
  | t₁, t₂ =>
    if t₁ == t₂ then some sorry
    else none

Edward Ayers (May 31 2022 at 14:47):

Sounds like you want to derive DecidableEq TType

Remi (May 31 2022 at 14:51):

@Edward Ayers Thanks, that exactly what I want!

Edward Ayers (May 31 2022 at 14:55):

You can do something like this:

variable {TType : Type u} [DecidableEq TType]
def TType.eq (t₁ t₂ : TType) : Option (t₁ = t₂) :=
  if h : t₁ = t₂ then some h else none

Unfortunately that doesn't quite work because Option only accepts types and not props. But once you have the if h : P then A else B pattern where Decidable P you can do a lot.

Also have a look at this section of TPIL: https://leanprover.github.io/theorem_proving_in_lean4/type_classes.html?highlight=Decidable#decidable-propositions

Chris Lovett (Aug 23 2022 at 19:42):

Why doesn't this work:

#eval (List String).nil

I realize I can use literal syntax and do this ([]: List String) but I'm just wondering what the deep compiler reason is to disallow the syntax I've written here. I'm confused why I can't declare the type, put it in parens and call the nil constructor to get back a typed empty list.

Seems type classes have the same limitation:

#eval (Add Nat).add 1 2

and this doesn't work either:

def Foo := List String
#eval Foo.cons "hello" ["a", "b", "c"]

But I can write this:

#eval ["a", "b", "c"].cons "d"

and this:

def emptyListOfStrings : List String := List.nil
#check emptyListOfStrings   -- List String

So it works when the type is implicit or can be inferred, and so I guess I'd understand better if the type argument to list was declared implicitly instead of explicitly ...

Reid Barton (Aug 23 2022 at 19:44):

The useless reason is that there's no reason to think that your non-working examples should work.

Reid Barton (Aug 23 2022 at 19:45):

Note in your working examples you have, before the ., either a value (["a", "b", "c"]) or a namespace (List).

Reid Barton (Aug 23 2022 at 19:47):

In the former case, because ["a", "b", "c"] : List String, ["a", "b", "c"].cons means List.cons.

Jireh Loreaux (Aug 23 2022 at 19:47):

so #eval (List.nil : List String) would work, right? (I'm not in Lean 4 at the moment.)

Chris Lovett (Aug 23 2022 at 19:50):

Yeah, I know all the variations that work, I'm just trying to figure out what is wrong with my understanding of inductive types that makes me think I should be able to #eval (List String).nil. Note that I cannot call nil on a list value (like I can with x.cons) since the nil constructor takes no arguments.

Reid Barton (Aug 23 2022 at 19:50):

(List String).nil should refer to Type.nil, I guess

Mario Carneiro (Aug 23 2022 at 19:56):

Keep in mind that List.nil and (List).nil are two completely different things. The first one is a single token, a namespaced name, and the second one is the |>.nil operation applied to the expression List

Mario Carneiro (Aug 23 2022 at 19:57):

This is somewhat confused by the fact that x.nil (where x is a local variable) is ambiguous between both of them, and there is some complexity in name resolution due to this

Chris Lovett (Aug 23 2022 at 20:07):

Thanks, the fact that (List).nil gives the same error is helpful. Perhaps the type argument on List is not really a type argument, it is some sort of type "context" that can only be inferred. At least lean is very consistent about this, I can't do this either:

structure Point (α : Type u) :=
  x : α
  y : α
  deriving Repr

#eval (Point Float).mk 5 7              -- same error

#eval (Point.mk 5 7 : Point Float) -- { x := 5.000000, y := 7.000000 }

Reid Barton (Aug 23 2022 at 20:08):

So for example Nat.zero is a namespaced name (zero in namespace Nat) that has nothing to do with the type Nat--except that the same inductive command defined both of them

Reid Barton (Aug 23 2022 at 20:11):

Chris Lovett said:

Perhaps the type argument on List is not really a type argument, it is some sort of type "context" that can only be inferred.

The type argument in List String really is a type argument. But List in List.nil is not a type at all

Chris Lovett (Aug 23 2022 at 20:12):

And for consistency you can't write (Nat).zero either.

Chris Lovett (Aug 23 2022 at 20:13):

Well the members of an inductive type are called "constructors" in TPIL. So List.nil should be constructing a List but it can't resolve the required type parameter, so you get the unresolved type List.nil : List ?m.10448.

Chris Lovett (Aug 23 2022 at 20:14):

And I was thinking why can't I help the compiler resolve the missing type by providing it with (List String).nil but alas, parens are special and dot notation doesn't like them.

Reid Barton (Aug 23 2022 at 20:14):

No, it has nothing to do with parentheses

Reid Barton (Aug 23 2022 at 20:16):

You are inventing some interpretation of List.nil that does not exist in Lean.

Chris Lovett (Aug 23 2022 at 20:19):

That's a good way to put it. All inductive type constructors must then be only "Name.ctor" where Name is the inductive type name and ctor is the constructor name, like Weekday.Monday in TPIL. But if the inductive type has one or more type parameters, those types must be inferred as they cannot be passed directly in the inductive type constructor call.

Chris Lovett (Aug 23 2022 at 20:19):

Oh, wait, yes it can with this #check List.nil (α := Float) -- : List Float interesting...

Reid Barton (Aug 23 2022 at 20:19):

Maybe it's not clear what inductive actually does: the inductive definition for List creates three new identifiers List, List.nil, List.cons (and a bunch of other stuff). List.nil has List as part of its name (more precisely, it is in the List namespace).

Reid Barton (Aug 23 2022 at 20:20):

List.nil doesn't mean "give me something called nil of type List", it is simply the identifier List.nil.

Chris Lovett (Aug 23 2022 at 20:21):

Well TPIL calls it an inductive type "constructor" so I don't want to stray too far from that definition.

Chris Lovett (Aug 23 2022 at 20:22):

So I read List.nil as construct a List using the nil constructor.

Reid Barton (Aug 23 2022 at 20:22):

Well, that's not how it works :upside_down:

Chris Lovett (Aug 23 2022 at 20:23):

Oh?

Reid Barton (Aug 23 2022 at 20:23):

It just means: the identifier List.nil.

Reid Barton (Aug 23 2022 at 20:24):

You could imagine a version of inductive that instead creates constructors called List_nil and List_cons, and then the way you would construct an empty list is using List_nil--but it would work exactly the same way.

Mario Carneiro (Aug 23 2022 at 20:25):

The C++ analogue would be something like List::nil()

Mario Carneiro (Aug 23 2022 at 20:26):

this is not the same as List.nil() which is a method applied to an object called List

Mario Carneiro (Aug 23 2022 at 20:27):

The List in List::nil is just a namespace, not an object. it's a way to construct fancy segmented names but not otherwise a thing in its own right

Mario Carneiro (Aug 23 2022 at 20:29):

In lean the first one is spelled List.nil and the second is (List).nil or List |>.nil (and this latter thing doesn't work because there isn't a method Type.nil that would apply to List itself)

Chris Lovett (Aug 23 2022 at 20:29):

I'm sure that all the object oriented programming I've done is where my problems are coming from so switching to C++ doesn't help because there I can call the constructor on the fully qualified type to create an empty list with auto x = list<float>();

Mario Carneiro (Aug 23 2022 at 20:30):

The analogue of calling the constructor on the fully qualified type is @List.nil Float

Chris Lovett (Aug 23 2022 at 20:30):

But I cannot call the constructors on a fully qualified inductive type like (List String)

Mario Carneiro (Aug 23 2022 at 20:30):

or (.nil : List String)

Chris Lovett (Aug 23 2022 at 20:31):

thanks and I also found List.nil (α := Float) earlier.

Chris Lovett (Aug 23 2022 at 20:32):

This one (.nil : List String) doesn't count in my mind because it is depending on type inference. I was looking for a syntax that did not depend on type inference. The @ one is interesting, but probably not for beginners? I think the closest so far is List.nil (α := Float)

Mario Carneiro (Aug 23 2022 at 20:37):

The @ syntax is the most straightforward, even for beginners, although you might want to prefer the other methods for style reasons

Mario Carneiro (Aug 23 2022 at 20:37):

If there are typeclass arguments you will need a lot of _ when using @

Reid Barton (Aug 23 2022 at 20:38):

What makes this confusing is:

  • The dot is used in two different syntactic constructs, building namespaced names (List.nil) and also "dot notation" (["a", "b", "c"].cons "d").
  • In Lean, types are also expressions, so the type List is something that it would make sense to use dot notation on (at least in principle). However, that's not what's going on in List.nil, which is a namespaced name.
  • The inductive command puts the constructors in a namespace named after the type being created. (Likewise, hand-written definitions relating to the List type are by convention put in the List namespace.) That opens the possibility of misinterpreting List.nil as involving the type List somehow.

Mario Carneiro (Aug 23 2022 at 20:38):

It's the most direct analogue of your list<string>() example

Jireh Loreaux (Aug 23 2022 at 20:38):

It wouldn't make much sense to call a constructor on List String. Think about this: modulo differences that don't matter List (α : Type) → Type, so List eats a type and spits out another type. Thus List String : Type. If you were going to have a function that takes List String as an argument and returns something (like the List.nil) of that type, such a function would have to have type Type → List String. How would such a function behaves on types other than List String?

Mario Carneiro (Aug 23 2022 at 20:40):

This also explains why if you want to have List String involved in the syntax you need to use type inference, because the constructor isn't taking List String as the argument, the argument is String and the resulting type is List String

Leonardo de Moura (Aug 23 2022 at 20:46):

BTW, our LSP server makes it clear which interpretation was used for the .s. You have to use a color theme that distinguishes the relevant syntactic categories or customize one.
image.png

  • List.nil is white because it is a constant.
  • val and values are yellow because they are parameters (or local variables).
  • cons is purple because it is part of the dot-notation. values.cons val is syntax sugar List.cons val values. If we hover over the elements, you will also get similar information.

Patrick Massot (Aug 23 2022 at 20:49):

Do we have a guide of relevant syntactic categories? I start all my Lean4 files with set_option autoImplicit false because my color theme isn't good enough at telling me when a typo triggers autoImplicit while I meant to name some existing thing.

Leonardo de Moura (Aug 23 2022 at 20:52):

@Patrick Massot The key syntactic categories for Lean are variable (for highlighting local variables and parameters) and property (for highlighting the dot notation). Very few color themes handle them out of the box :(

Leonardo de Moura (Aug 23 2022 at 20:54):

You can configure an existing theme by editing your settings.json.

Patrick Massot (Aug 23 2022 at 20:54):

I found the previous discussion in https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/.E2.9C.94.20VS.20Code.20color.20scheme. I'll try to write a useful summary

Leonardo de Moura (Aug 23 2022 at 20:54):

Here is my config

    "editor.semanticHighlighting.enabled": true,
    "workbench.colorCustomizations": {
      "[Solarized Light]": {"editor.selectionHighlightBackground": "#e9dcc5"}
    },
    "editor.semanticTokenColorCustomizations": {
        "[Solarized Light]": {"rules": {"function": "#c1892f", "property": "#69878c"}},
        "[Ayu Dark]": {"rules": {"property": "#948fd0", "variable": "#cbc248"}}
    },

Leonardo de Moura (Aug 23 2022 at 20:55):

Patrick Massot said:

I found the previous discussion in https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/.E2.9C.94.20VS.20Code.20color.20scheme. I'll try to write a useful summary

Thanks! We will add it to the manual.

Chris Lovett (Aug 23 2022 at 21:05):

Leo made an interesting point that is helpful: values.cons val is actually List.cons val values. I was thinking of List as a sort of generic type (in the C++ sense) that can't reallybe constructed until you provide the type parameters, and List String then as a specialization of that same type and therefore it inherits all the methods that List has, including the constructors and this is simply not the case. So, the fact that you can write #eval ["a", "b"].cons "c" -- ["c", "a", "b"] is a little misleading because it makes it appear that List String has a cons constructor, but it doesn't.

Chris Lovett (Aug 23 2022 at 21:11):

Building on all the interesting talk about namespaces above, I can extend the List.String namespace and add this:

namespace List.String
def nil : List String := []
end List.String

#eval List.String.nil  -- []
#check List.String.nil  --List String

but obviously I don't want to do that for every possible type of list...

Reid Barton (Aug 23 2022 at 21:22):

Likewise, you could also do

namespace Nat
def nil : List String := []
end Nat

#eval Nat.nil  -- []
#check Nat.nil  --List String

Mauricio Collares (Aug 23 2022 at 21:25):

The List.String namespace was empty before this, right?

Mauricio Collares (Aug 23 2022 at 21:28):

If not, that gives me a strong vector<bool> vibe

Jireh Loreaux (Aug 23 2022 at 21:29):

Again, the above List.String.nil is just an identifier; it's not doing anything fancy.

Mauricio Collares (Aug 23 2022 at 21:34):

Right, I should have said "there are no other List.String-prefixed identifiers, right?". Thanks for the correction.

Jireh Loreaux (Aug 23 2022 at 21:37):

Sorry Mauricio, my comment was intended for aiding Chris's understanding.

Chris Lovett (Aug 23 2022 at 22:08):

I hear what you are saying about "List.nil" is just an identifier and "List.String.nil" is just an identifier and so on, but it is not satisfying given that in every other language "." is special. If I followed your statement to its logical conclusion, I would think it is perfectly fine to write this function:

def Frump...alump (x : Nat) := x * x            -- unknown identifier 'Frump'

But alas I cannot. So "." in an Identifier is special. It is a namespace separator.

Reid Barton (Aug 23 2022 at 22:15):

Yes exactly. But the List namespace has no relation to the List type, except by convention (and how the inductive command works).

Mario Carneiro (Aug 23 2022 at 22:18):

. in identifiers is special, but only to give a hierarchical structure to identifiers. . is not an "identifier character" so you can't directly write a..b as an ident

Mario Carneiro (Aug 23 2022 at 22:20):

Without such structure it's hard to have commands like open that allow you to omit namespaces in an identifier

Chris Lovett (Aug 23 2022 at 22:25):

I love using "." in namespace qualified names. I'm glad Lean can do the same. Note that TPIL does indeed call the List inductive type a namespace, with this:

The constructors all live in the Weekday namespace.

Jireh Loreaux (Aug 23 2022 at 22:27):

No, List the namespace and List the inductive type are different, they just happen to share the same four English letters. Nevertheless, the constructors for List the inductive type do live in the List namespace.

Chris Lovett (Aug 23 2022 at 23:56):

Perhaps you are talking implementation details, or are you saying the book TPIL is wrong when it says "The constructors all live in the Weekday namespace" ?

Reid Barton (Aug 24 2022 at 00:06):

The book is correct, the constructs do live in the Weekday namespace.

Reid Barton (Aug 24 2022 at 00:07):

The Weekday type and the Weekday namespace are not the same thing.

Chris Lovett (Aug 24 2022 at 00:27):

Well it's tricky because in the book the Weekday inductive type and all its constructors are defined BEFORE any explicit creation of namespace Weekday and in fact even before defining namespace Weekday the code was then able to open Weekday and open is defined to only work on namespaces, therefore the inductive type Weekday created a namespace of the same name, but we are quibbling now, so diminishing returns, but thanks for all the excellent thoughts and clarifications.

Leonardo de Moura (Aug 24 2022 at 00:36):

@Chris Lovett The book says: "The inductive command creates a new type, Weekday. The constructors all live in the Weekday namespace." It looks clear to me that a namespace called "Weekday" was also created. Otherwise, how would we add the constructors to the namespace "Weekday"?
Any suggestions on how to make it clear that a namespace "Weekday" is also being created? Or is it not clear at this point in the book that namespaces and types are different things?

Reid Barton (Aug 24 2022 at 00:36):

I think a namespace is "created" (in the sense that you can open it) as soon as any identifier is defined in that namespace; in any case, the inductive Weekday [...] command certainly creates the Weekday namespace, as well as the Weekday type (and various other things).

Chris Lovett (Aug 24 2022 at 00:54):

I think it would be nice to explicitly state somewhere that defining and inductive type creates both a type and a namespace of that same name. This avoids confusion with other languages where a type name is a namespace which then avoids my original confusion thinking (List String) is a namespace that I could .cons or .nil into. Question, does a type class also create a namespace of the same name? What about a structure?

Leonardo de Moura (Aug 24 2022 at 00:56):

From TPIL: "The structure command is essentially a "front end" for defining inductive data types. Every structure declaration introduces a namespace with the same name. The general form is as follows:"

Leonardo de Moura (Aug 24 2022 at 00:57):

https://leanprover.github.io/theorem_proving_in_lean4/structures_and_records.html#declaring-structures

Chris Lovett (Aug 24 2022 at 01:01):

that language is perfect, and I assume the same language could be used in the chapter on inductive types, and type classes?

Chris Lovett (Aug 27 2022 at 05:28):

How come Repr doesn't provide ToString?

structure Config where
  help : Bool := false
  verbose : Bool := false
  input : String := ""
  output : String := ""
  deriving Repr

#eval ({} : Config)
-- { help := false, verbose := false, input := "", output := "" }

But I can't seem to do IO.println config nor can I IO.println s!"{config}" ? Do I have to also create a ToString instance on this? I see stuff like this in the Lean code base:

def Stats.toString (s : Stats) : String :=
  s!"\{nodes := {s.numNodes}, depth := {s.depth}, tail size := {s.tailSize}}"

instance : ToString Stats := Stats.toString

But what's the point of Repr if we have to do this also?

Mario Carneiro (Aug 27 2022 at 05:31):

ToString and Repr have slightly different purposes, roughly comparable to Rust's Display vs Debug. ToString is for a human-readable display of the string, while Repr is supposed to be (mostly) suitable for copy-pasting as lean code

Chris Lovett (Aug 27 2022 at 05:31):

Ok, and there's no helpers for ToString on a structure? I have to do it by hand?

Mario Carneiro (Aug 27 2022 at 05:31):

for instance, the ToString instance for strings just spits the string back out, while the Repr instance puts quotes and backslashes in

Mario Carneiro (Aug 27 2022 at 05:32):

And also like Rust, the derive handler only exists for Repr, with the ToString instance intended for manual implementation

Mario Carneiro (Aug 27 2022 at 05:33):

If you would like to use the same ToString as Repr, you can derive Repr and then instance : ToString Foo := \<repr\>

Chris Lovett (Aug 27 2022 at 05:42):

structure Config where
  help : Bool := false
  verbose : Bool := false
  input : String := ""
  deriving Repr

instance : ToString Config :=  repr

gives an error

type mismatch
  ?m.2361  Std.Format
has type
  Sort (max 1 ?u.2357) : Type (max 1 ?u.2357)
but is expected to have type
  ToString Config : Type

I searched the lean code for ⟨repr⟩ but found nothing like that...

Sebastian Ullrich (Aug 27 2022 at 08:09):

That's a terrifying error message, but I can't reproduce it

application type mismatch
  { toString := repr }
argument
  repr
has type
  ?m.1683  Lean.Format : Type ?u.1682
but is expected to have type
  Config  String : Type

Last updated: Dec 20 2023 at 11:08 UTC