michael/csci8980-f21
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

twiddled imports for PreorderReasoning

Browse source
This commit is contained in:
Philip Wadler 2017-06-27 15:52:07 +01:00
parent ba15881340
commit 6c4fa4bf72
1 changed files with 3 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/Stlc.lagda
View file

@ -18,6 +18,8 @@ open import Data.Bool using (Bool; true; false; if_then_else_)
open import Relation.Nullary using (Dec; yes; no) open import Relation.Nullary using (Dec; yes; no)
open import Relation.Nullary.Decidable using (⌊_⌋) open import Relation.Nullary.Decidable using (⌊_⌋)
open import Relation.Binary.PropositionalEquality as P using (_≡_; _≢_; refl) open import Relation.Binary.PropositionalEquality as P using (_≡_; _≢_; refl)
open import Relation.Binary using (Preorder)
import Relation.Binary.PreorderReasoning as PreorderReasoning
-- open import Relation.Binary.Core using (Rel) -- open import Relation.Binary.Core using (Rel)
-- open import Data.Product using (∃; ∄; _,_) -- open import Data.Product using (∃; ∄; _,_)
-- open import Function using (_∘_; _$_) -- open import Function using (_∘_; _$_)
@ -128,8 +130,6 @@ _⟹*_ = (_⟹_) *
\end{code} \end{code}
\begin{code} \begin{code}
open import Relation.Binary using (Preorder)
⟹*-Preorder : Preorder _ _ _ ⟹*-Preorder : Preorder _ _ _
⟹*-Preorder = record ⟹*-Preorder = record
{ Carrier = Term { Carrier = Term
@ -142,7 +142,7 @@ open import Relation.Binary using (Preorder)
} }
} }
open import Relation.Binary.PreorderReasoning ⟹*-Preorder open PreorderReasoning ⟹*-Preorder
using (begin_; _∎) renaming (_≈⟨_⟩_ to _≡⟨_⟩_; _∼⟨_⟩_ to _⟹*⟨_⟩_) using (begin_; _∎) renaming (_≈⟨_⟩_ to _≡⟨_⟩_; _∼⟨_⟩_ to _⟹*⟨_⟩_)
\end{code} \end{code}