Zulip Chat Archive

Stream: new members

Topic: inhabited list types.

Ocschwar (Dec 17 2021 at 20:28):

Hi, all. I am using the parser to read a text file to get a list of structure s that I defined ( https://github.com/ocschwar/adventofcode/blob/master/src/aoc/day2.lean) for advent of code. )

Because I'm a neophyte and the parser was cut and pasted from an earlier zulip chat (thanks again!), the parsing function returns type list (list instruction)and I need to convert it to list instruction

The dumb way below is failing:
The equivalent code for a list of naturals worked fine. This is failing with

failed to synthesize type class instance for
dayinput : list (list instruction),
_x : unit
 inhabited instruction

what should I be doing to assure the type setting that the parse_file function is returning a list of inhabited lists?

Horatiu Cheval (Dec 17 2021 at 20:40):

The problem is that you haven't proved that the type instruction has any terms

Horatiu Cheval (Dec 17 2021 at 20:41):

You can probably do this automatically be writing @[derive inhabited] before the definition of your instruction type.

Horatiu Cheval (Dec 17 2021 at 20:41):

Something like this, after briefly looking at your code

import tactic

@[derive inhabited]
inductive comd : Type
| up : comd
| down : comd
| forward : comd

@[derive inhabited]
structure instruction :=
(comd : comd )
(length :  )

Ocschwar (Dec 17 2021 at 20:45):

(copy, paste, watch the red disappear). That worked! Thanks!

Horatiu Cheval (Dec 17 2021 at 20:47):

Or if you prefer to show the inhabitedness yourself to see what it actually means, it's enough to provide some term of type instruction

instance : inhabited instruction := _ -- put any term of type `instruction` instead of _

For instance

instance : inhabited instruction := instruction.mk comd.up 0

Ocschwar (Dec 17 2021 at 21:15):

I'll use the syntax for has_t_string

Last updated: Dec 20 2023 at 11:08 UTC