Questions tagged [guarded-recursion]
Cubical Agda is extended with Nakano’s later modality and guarded recursion based on Ticked Cubical Type Theory. (from Agda)
3 questions
6
votes
2
answers
260
views
Is there a formalism of "coinductive" data types with negative occurrences?
Consider the following program in Haskell:
...
1
vote
1
answer
132
views
How do I work with ints when using coq-of-ocaml for OCaml to Coq conversion?
I am trying to use coq-of-ocaml to convert a simple recursive factorial function written in OCaml into Coq. I have a testing_factorial.ml file which defines the ...
8
votes
1
answer
160
views
Are `P x` and `▸ ((next P) ⊛ (next x))` equivalent in Guarded Cubical Agda?
In Guarded Cubical Agda there's ▹_ : Set i → Set i and ▸_ : ▹ Set i → Set i.
If I've got ...
- 1,001