lean4-htt/src/Init/Data.lean
2020-06-25 13:26:16 -07:00

20 lines
497 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.Option
import Init.Data.Random