Card game encoding with dependent types

Stream: general

[Diego Antonio Rosario Palomino]

Hello back lean4 community. I have been contracted to write the digital version of a tcg ( think games like yu gi oh and magic the gathering )

I have previously look into programming such a game in haskell and got the following resources :
https://docs.google.com/document/d/1CTJsixtT9aGqH7Va0f98-trfWb1qxB1bLHJdda1jUM0/edit?usp=drive_link

I am wondering if anyone has an idea on implementing such card games that would make use of dependent types as in lean 4. Or whether this is a field where the dependent types subset in haskell ( GADTS among other features ) are enough