diff options
| author | Helmut Grohne <helmut@subdivi.de> | 2012-12-14 12:03:04 +0100 |
|---|---|---|
| committer | Helmut Grohne <helmut@subdivi.de> | 2012-12-14 12:03:04 +0100 |
| commit | 06e16ec6a913f216ef43a3a32e7094c6e83d40ef (patch) | |
| tree | 22db8656f3e50a7762dfa0b66f2f730db1aade72 /Precond.agda | |
| parent | d39092a7bfe8180b5928aff7ec783de3c48b62f4 (diff) | |
| download | bidiragda-06e16ec6a913f216ef43a3a32e7094c6e83d40ef.tar.gz | |
un-inline different-drop
Diffstat (limited to 'Precond.agda')
| -rw-r--r-- | Precond.agda | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/Precond.agda b/Precond.agda index 44512b3..76875a7 100644 --- a/Precond.agda +++ b/Precond.agda @@ -56,7 +56,7 @@ different-∉ x (y ∷ ys) p (there pxs) = different-∉ x ys (different-drop y different-assoc : {m n : ℕ} → (u : Vec (Fin n) m) → (v : Vec Carrier m) → all-different u → ∃ λ h → assoc u v ≡ just h different-assoc [] [] p = empty , refl -different-assoc (u ∷ us) (v ∷ vs) p with different-assoc us vs (λ i j i≢j → p (suc i) (suc j) (i≢j ∘ suc-injective)) +different-assoc (u ∷ us) (v ∷ vs) p with different-assoc us vs (different-drop u us p) different-assoc (u ∷ us) (v ∷ vs) p | h , p' = insert u v h , (begin assoc (u ∷ us) (v ∷ vs) ≡⟨ refl ⟩ |