Mercurial > hg > Papers > 2020 > ryokka-master
view paper/src/axiom-taut.agda @ 2:c7acb9211784
add code, figure. and paper fix content
author | ryokka |
---|---|
date | Mon, 27 Jan 2020 20:41:36 +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