~ubuntu-branches/ubuntu/wily/agda-stdlib/wily

« back to all changes in this revision

Viewing changes to src/Relation/Binary/List/StrictLex.agda

• browse files at revision 9
• compare with another revision
• download diff
• download tarball
• view history from revision 9

Show diffs side-by-side

added

removed

src/Relation/Binary/List/StrictLex.agda

24

24

open import Relation.Binary.List.Pointwise as Pointwise

25

25

   using ([]; _∷_; head; tail)

26

26

 

27

 

private

28

 

 module Dummy {A : Set} where

 

27

module _ {A : Set} where

29

28

 

30

29

  data Lex (P : Set) (_≈_ _<_ : Rel A zero) : Rel (List A) zero where

31

30

    base : P                             → Lex P _≈_ _<_ []       []

282

281

    ; <-resp-≈      = respects₂ isEquivalence <-resp-≈

283

282

    } where open IsStrictTotalOrder sto

284

283

 

285

 

open Dummy public

286

 

 

287

284

-- "Packages" (e.g. preorders) can also be handled.

288

285

 

289

286

≤-preorder : Preorder _ _ _ → Preorder _ _ _

• Older »

Loggerhead is a web-based interface for Breezy
Version: 2.0.1