module Prelude where

{- Some (more or less) standard library definitions
   for use with the WSLN library. -}

open import Prelude.Level public
open import Prelude.Instance public
open import Prelude.Notation public
open import Prelude.Function public
open import Prelude.Identity public
open import Prelude.Unit public
open import Prelude.Empty public
open import Prelude.Sum public
open import Prelude.WellFounded public

open import Prelude.Product public
open import Prelude.BiImplication public

open import Prelude.List public
open import Prelude.Nat public
open import Prelude.Vec public
open import Prelude.Fin public
open import Prelude.FinInt public

open import Prelude.Decidable public

open import Prelude.Prop public