{-# OPTIONS --type-in-type #-}

module BouncingBall where

open import NeilPrelude
open import Real
open import Bool

------------------------------------------

Acceleration = ℜ
Velocity = ℜ
Height = ℜ

Ball = Height × Velocity

postulate g : Acceleration

------------------------------------------

detectImpact : Ball → Bool
detectImpact (h , v) = (h <= O) ∧ (v <, O)

negateVel : Ball → Ball
negateVel (h , v) = (h , negate v)

------------------------------------------