lean4-htt/src/Init/Data.lean

43 lines
1 KiB
Text

/-
Copyright (c) 2016 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
prelude
import Init.Data.Basic
import Init.Data.Nat
import Init.Data.Bool
import Init.Data.BitVec
import Init.Data.Cast
import Init.Data.Char
import Init.Data.String
import Init.Data.List
import Init.Data.Int
import Init.Data.Array
import Init.Data.Array.Subarray.Split
import Init.Data.ByteArray
import Init.Data.FloatArray
import Init.Data.Fin
import Init.Data.UInt
import Init.Data.Float
import Init.Data.Option
import Init.Data.Ord
import Init.Data.Random
import Init.Data.ToString
import Init.Data.Range
import Init.Data.Hashable
import Init.Data.OfScientific
import Init.Data.Format
import Init.Data.Stream
import Init.Data.Prod
import Init.Data.AC
import Init.Data.Queue
import Init.Data.Channel
import Init.Data.Sum
import Init.Data.BEq
import Init.Data.Subtype
import Init.Data.ULift
import Init.Data.PLift
import Init.Data.Zero
import Init.Data.NeZero
import Init.Data.Function