annotate paper/src/axiom-taut.agda.replaced @ 2:c7acb9211784
add code, figure. and paper fix content
| author |
ryokka |
| date |
Mon, 27 Jan 2020 20:41:36 +0900 |
| parents |
|
| children |
b5fffa8ae875 |
| rev |
line source |
|
2
|
1 _@$\Rightarrow$@_ : Bool → Bool → Bool
|
|
|
2 false @$\Rightarrow$@ _ = true
|
|
|
3 true @$\Rightarrow$@ true = true
|
|
|
4 true @$\Rightarrow$@ false = false
|
|
|
5
|
|
|
6 Axiom : Cond @$\rightarrow$@ PrimComm @$\rightarrow$@ Cond @$\rightarrow$@ Set
|
|
|
7 Axiom pre comm post = ∀ (env : Env) → (pre env) @$\Rightarrow$@ ( post (comm env)) @$\equiv$@ true
|
|
|
8
|
|
|
9 Tautology : Cond @$\rightarrow$@ Cond @$\rightarrow$@ Set
|
|
|
10 Tautology pre post = ∀ (env : Env) → (pre env) @$\Rightarrow$@ (post env) @$\equiv$@ true
|
