diff options
| author | Helmut Grohne <helmut@subdivi.de> | 2012-04-19 11:52:27 +0200 |
|---|---|---|
| committer | Helmut Grohne <helmut@subdivi.de> | 2012-04-19 11:52:27 +0200 |
| commit | 7c3e2c61e55aa876f88fbd34c94ccfb0a8c715d4 (patch) | |
| tree | da62a6b97b8744c0bb7b9067b9007a8960004246 /Bidir.agda | |
| parent | dabd8455638d0cea486dd94dcdd13729077018d7 (diff) | |
| download | bidiragda-7c3e2c61e55aa876f88fbd34c94ccfb0a8c715d4.tar.gz | |
move lemma-just!=nothing to FinMap and use it there
Diffstat (limited to 'Bidir.agda')
| -rw-r--r-- | Bidir.agda | 3 |
1 files changed, 0 insertions, 3 deletions
@@ -66,9 +66,6 @@ lemma-checkInsert-wrong eq i x m x' d refl | .(just x') with eq x x' lemma-checkInsert-wrong eq i x m x' d refl | .(just x') | yes q = contradiction q d lemma-checkInsert-wrong eq i x m x' d refl | .(just x') | no ¬q = refl -lemma-just≢nothing : {A Whatever : Set} {a : A} → _≡_ {_} {Maybe A} (just a) nothing → Whatever -lemma-just≢nothing () - record checkInsertEqualProof {A : Set} {n : ℕ} (eq : EqInst A) (i : Fin n) (x : A) (m : FinMapMaybe n A) (e : Maybe (FinMapMaybe n A)) : Set where field same : lookupM i m ≡ just x → just m ≡ e |