Coqc doesn't recognise !! operator

antalsz / hs-to-coq

Convert Haskell source code to Coq source code

https://hs-to-coq.readthedocs.io

MIT License

279 stars 27 forks source link

Open christinaburge opened 4 years ago

christinaburge commented 4 years ago

I have the !! operator in my Haskell code:

diag xs = zipWith (!!) xs [0..3]

Hs-to-coq will translate this

Definition diag := 40 fun xs => GHC.List.zipWith _GHC.List.!!_ xs (GHC.Enum.enumFromTo #0 #3).

but then the coqc compiler does not recognise the translation:

Error: Cannot infer an existential variable of type "Type"