From 76d21900a237a91e302d250f54f1d8475826a5a9 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 2 Oct 2014 11:10:37 -0700 Subject: [PATCH] feat(library): add aliases for some sorts --- library/standard.lean | 2 +- library/type.lean | 7 +++++++ 2 files changed, 8 insertions(+), 1 deletion(-) create mode 100644 library/type.lean diff --git a/library/standard.lean b/library/standard.lean index 6e28175c65..68fdba1c64 100644 --- a/library/standard.lean +++ b/library/standard.lean @@ -7,4 +7,4 @@ -- The constructive core of Lean's library. -import logic data tools.tactic +import type logic data tools.tactic diff --git a/library/type.lean b/library/type.lean new file mode 100644 index 0000000000..bdbc8fc664 --- /dev/null +++ b/library/type.lean @@ -0,0 +1,7 @@ +-- Copyright (c) 2014 Microsoft Corporation. All rights reserved. +-- Released under Apache 2.0 license as described in the file LICENSE. +-- Authors: Leonardo de Moura + +definition Type₁ [reducible] := Type.{1} +definition Type₂ [reducible] := Type.{2} +definition Type₃ [reducible] := Type.{3}