Very interesting find here IMO. @jmw150 Have you seen this yet?
http://comonad.com/reader/2022/internalized-guarded-recursion-for-equational-reasoning/
@johnabs
So he found a decidable fragment. These are pretty common. But it is pretty neat that it is already part of Haskell's category flavored logic system.
QOTO: Question Others to Teach Ourselves An inclusive, Academic Freedom, instance All cultures welcome. Hate speech and harassment strictly forbidden.
@johnabs
So he found a decidable fragment. These are pretty common. But it is pretty neat that it is already part of Haskell's category flavored logic system.