Converting haskell to lean

Stream: general

[Colten Gaines]

Howdy all, this is my first time using the zulip chat so hopefully I have posted my question in the correct area. I am currently doing some research with the University of Wyoming on lean and I wanted to convert some existing haskell code to lean. For example Im not really sure how to convert this piece of haskell code
data House = House { color :: Color -- <trait> :: House -> <Trait> , man :: Man , pet :: Pet , drink :: Drink , smoke :: Smoke } data Color = Red | Green | Blue | Yellow | White
so on and so forth defining all the separate datatypes to form the House datatype

Im sure its really simple but Im struggling to find the answer in TPiL

Thanks all

[Mario Carneiro]

The first one is a structure, the second one is an inductive

[Mario Carneiro]

structure House :=
(color : Color)
(man : Man)
(pet : Pet)
(drink : Drink)
(smoke : Smoke)

inductive Color
| Red | Green | Blue | Yellow | White