Mercurial > hg > Papers > 2020 > soto-midterm
view src/axiom-taut.agda @ 1:73127e0ab57c
(none)
author | soto@cr.ie.u-ryukyu.ac.jp |
---|---|
date | Tue, 08 Sep 2020 18:38:08 +0900 |
parents | |
children |
line wrap: on
line source
_⇒_ : Bool → Bool → Bool false ⇒ _ = true true ⇒ true = true true ⇒ false = false Axiom : Cond -> PrimComm -> Cond -> Set Axiom pre comm post = ∀ (env : Env) → (pre env) ⇒ ( post (comm env)) ≡ true Tautology : Cond -> Cond -> Set Tautology pre post = ∀ (env : Env) → (pre env) ⇒ (post env) ≡ true