larrytheliquid

open import Data.Nat
open import Data.Fin renaming ( zero to here ; suc to there )
open import Data.Product
open import Relation.Binary.PropositionalEquality
module _ where

mutual
 data Vec₁ (A : Set) : ℕ → Set where
   nil₁ : Vec₁ A zero
   cons₁ : {n : ℕ} → A → (xs : Vec₁ A n) → toℕ (Vec₂ xs) ≡ n → Vec₁ A (suc n)

larrytheliquid

open import Data.Nat
open import Data.Product
open import Data.String
open import Relation.Binary.PropositionalEquality
module _ where

mutual
  data Vec₁ (A : Set) : Set where
    nil : Vec₁ A
    cons : (n : ℕ) → A → (xs : Vec₁ A) → Vec₂ xs ≡ n → Vec₁ A

larrytheliquid

module Weed where

data ⊥ : Set where

magic : {A : Set} → ⊥ → A
magic ()

data Weed (A : Set) : Set where
  grow : (A → Weed A) → Weed A

larrytheliquid

module FSM where

data Bool : Set where true false : Bool

data List (A : Set) : Set where
  [] : List A
  _∷_ : A → List A → List A

----------------------------------------------------------------------