I am trying to model the following in Coq, which works fine in Haskell (below is Haskell code):
data Point = Pt Config Config data Line = Ln Point Point | Ext Line data Circle = Crc Point Line data Figure = P Point | L Line | C Circle type Config = [Figure] a = Pt   b = Pt  [P a] ln = Ln a b d = Pt [L ln] [P a, P b]
Basically, b is a distinct point from a, ln is the straight line going through a and b, and d is a point on line ln but distinct from a and from b. The problem is that Config depends on Point, Line and Circle, and then Point depends on Config. I have seen that mutually dependent types existed in Coq, but do they work after multiple levels of nesting or indirection like this?
If not, do you know another proof-assistant which allows such constructions?