Discussion:
Is this a recursive record?
(too old to reply)
Apostolis Xekoukoulotakis
2018-01-23 17:37:44 UTC
Permalink
Raw Message
I get an error that the specified record is recursive.
I don't understand why it is.

The code at the moment is full of holes and a bit difficult to read because
it is inside a big mutual block.

https://github.com/xekoukou/AgdaScript/blob/5fa8728c3c03d33c4b249a1c011958db6e0d36ae/AgdaScript2.agda#L50

Removing this line, stops the error from showing up.

https://github.com/xekoukou/AgdaScript/blob/5fa8728c3c03d33c4b249a1c011958db6e0d36ae/AgdaScript2.agda#L80
Nils Anders Danielsson
2018-01-24 08:21:52 UTC
Permalink
Raw Message
Post by Apostolis Xekoukoulotakis
I get an error that the specified record is recursive.
I don't understand why it is.
There seems to be a cycle AsFunF → AsFun → LFun → _⊂f_ → AsFunFT →
AsFunF.
--
/NAD
Loading...