← Back to branch summary

~ubuntu-branches/ubuntu/raring/agda-stdlib/raring

« back to all changes in this revision

Viewing changes to src/Relation/Binary/PreorderReasoning.agda

  • Committer: Package Import Robot
  • Author(s): Iain Lane
  • Date: 2013-04-10 10:30:20 UTC
  • mfrom: (2.1.7 experimental)
  • Revision ID: package-import@ubuntu.com-20130410103020-bcspfz3whyy5iafu
Tags: 0.7-1
* [6d52289] Imported Upstream version 0.7
* [54104d0] Update Depends and Build-Depends for this version, compatible
  with Agda 2.3.2
* [b3ddce4] No need for the .install file to be executable (thanks lintian)
* [a9a6cb7] Standards-Version → 3.9.4, no changes required

Show diffs side-by-side

added added

removed removed

Lines of Context:
src/Relation/Binary/PreorderReasoning.agda
32
32
 
33
33
infix  4 _IsRelatedTo_
34
34
infix  2 _∎
35
 
infixr 2 _∼⟨_⟩_ _≈⟨_⟩_
 
35
infixr 2 _∼⟨_⟩_ _≈⟨_⟩_ _≈⟨⟩_
36
36
infix  1 begin_
37
37
 
38
38
-- This seemingly unnecessary type is used to make it possible to
50
50
_≈⟨_⟩_ : ∀ x {y z} → x ≈ y → y IsRelatedTo z → x IsRelatedTo z
51
51
_ ≈⟨ x≈y ⟩ relTo y∼z = relTo (trans (reflexive x≈y) y∼z)
52
52
 
 
53
_≈⟨⟩_ : ∀ x {y} → x IsRelatedTo y → x IsRelatedTo y
 
54
_ ≈⟨⟩ x∼y = x∼y
 
55
 
53
56
_∎ : ∀ x → x IsRelatedTo x
54
57
_∎ _ = relTo refl