← Back to branch summary

~ubuntu-branches/ubuntu/wily/agda/wily-proposed

« back to all changes in this revision

Viewing changes to examples/outdated-and-incorrect/ProofRep.agda

  • Committer: Package Import Robot
  • Author(s): Iain Lane
  • Date: 2014-08-05 06:38:12 UTC
  • mfrom: (1.1.6)
  • Revision ID: package-import@ubuntu.com-20140805063812-io8e77niomivhd49
Tags: 2.4.0.2-1
* [6e140ac] Imported Upstream version 2.4.0.2
* [2049fc8] Update Build-Depends to match control
* [93dc4d4] Install the new primitives
* [e48f40f] Fix typo dev→doc

Show diffs side-by-side

added added

removed removed

Lines of Context:
examples/outdated-and-incorrect/ProofRep.agda
1
 
 
2
 
module ProofRep where
3
 
 
4
 
import Prelude
5
 
import Logic.Relations
6
 
import Logic.Identity
7
 
import Data.Nat
8
 
import Data.Nat.Properties
9
 
 
10
 
open Prelude
11
 
open Data.Nat hiding (_==_; _≡_)
12
 
open Data.Nat.Properties
13
 
open Logic.Relations
14
 
 
15
 
module Foo (Var : Set) where
16
 
 
17
 
  data _==_ : (x y : Var) -> Set where
18
 
    cRefl  : {x : Var} -> x == x
19
 
    cSym   : {x y : Var} -> y == x -> x == y
20
 
    cTrans : {x y z : Var} -> x == z -> z == y -> x == y
21
 
    cAxiom : {x y : Var} -> x == y
22
 
 
23
 
  data Axioms {A : Set}(_≈_ : Rel A)([_] : Var -> A) : Set where
24
 
    noAxioms   : Axioms _≈_ [_]
25
 
    anAxiom    : (x y : Var) -> [ x ] ≈ [ y ] -> Axioms _≈_ [_]
26
 
    manyAxioms : Axioms _≈_ [_] -> Axioms _≈_ [_] -> Axioms _≈_ [_]
27
 
 
28
 
  refl : {x : Var} -> x == x
29
 
  refl = cRefl
30
 
 
31
 
  sym : {x y : Var} -> x == y -> y == x
32
 
  sym (cRefl xy)     = cRefl (Var.sym xy)
33
 
  sym  cAxiom        = cSym cAxiom
34
 
  sym (cSym p)       = p
35
 
  sym (cTrans z p q) = cTrans z (sym q) (sym p)
36
 
 
37
 
  trans : {x y z : Var} -> x == y -> y == z -> x == z
38
 
  trans {x}{y}{z} (cRefl xy) q     = Var.subst (\w -> w == z) (Var.sym xy) q
39
 
  trans {x}{y}{z} p (cRefl yz)     = Var.subst (\w -> x == w) yz p
40
 
  trans {x}{y}{z} (cTrans w p q) r = cTrans w p (trans q r)
41
 
  trans           p q              = cTrans _ p q
42