SHARE
TWEET

Untitled

a guest Sep 22nd, 2019 88 Never
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
  1.  
  2. open import Relation.Binary.PropositionalEquality
  3. open import Data.Nat
  4. open import Data.Vec
  5. import Data.Nat.Properties as ℕₚ
  6.  
  7. data Split {ℓ} {A : Set ℓ} : ∀ {i j} → Vec A i → Vec A (i + j) → Vec A j → Set ℓ where
  8.   l_ : ∀ {i j x l m r} → Split {i = i} {j = j} l m r
  9.      → Split (x ∷ l) (x ∷ m) r
  10.   r_ : ∀ {i j x l m r} → Split {i = i} {j = j} l m r
  11.      → Split l (subst (Vec A) (sym (ℕₚ.+-suc _ _)) (x ∷ m)) (x ∷ r)
  12.   s : Split [] [] []
RAW Paste Data
We use cookies for various purposes including analytics. By continuing to use Pastebin, you agree to our use of cookies as described in the Cookies Policy. OK, I Understand
Not a member of Pastebin yet?
Sign Up, it unlocks many cool features!
 
Top