lean4-htt/src/Init/Data.lean
Leonardo de Moura e22af8d1ef feat: add FloatArray
cc @dselsam
2020-04-07 18:05:54 -07:00

25 lines
615 B
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.Char
import Init.Data.String
import Init.Data.List
import Init.Data.Int
import Init.Data.Array
import Init.Data.ByteArray
import Init.Data.FloatArray
import Init.Data.Fin
import Init.Data.UInt
import Init.Data.Float
import Init.Data.RBTree
import Init.Data.RBMap
import Init.Data.Option
import Init.Data.HashMap
import Init.Data.Random
import Init.Data.Queue
import Init.Data.Stack