inhabited list types.

Stream: new members

[Ocschwar]

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]

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

[Horatiu Cheval]

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

[Horatiu Cheval]

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]

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

[Horatiu Cheval]

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]

I'll use the syntax for has_t_string