Boolean-valued "check" function assuming input Stream
Created by: joaopizani
From @joaopizani on March 28, 2015 12:34
Based on smallcheck. Type more or less like:
check : ∀ {α β} → (α → β) → Stream α → Stream β → ℕ → Bool
Then we can have:
checkℂσ : ∀ {α β} ⦃ _ : ⇓W⇑ α ⦄ ⦃ _ : ⇓W⇑ β ⦄ → ℂ {σ} α β → Stream α → Stream β → ℕ → Bool
checkℂσ ⦃ sα ⦄ ⦃ sβ ⦄ c = check (⟦ c ⟧̂ ⦃ sα ⦄ ⦃ sβ ⦄)
Copied from original issue: joaopizani/piware#28