1:32 PM
new-tag A new tag coinduction was created by Javier. Edit summary: "Coinduction is a tag that people may look for and this question is very relevant in the area."
9
I've been exploring corecursion in Coq (specifically, infinite streams of natural numbers) lately and so far any coinductive predicate I've constructed and its coinductive proof can be transformed into an inductive predicate and an inductive proof with a proof that either style proof can be const...
« first day (2687 days earlier) ← previous day next day → last day (1642 days later) »