michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(library): add aliases for some sorts

Browse source
This commit is contained in:
Leonardo de Moura 2014-10-02 11:10:37 -07:00
parent 4cb54ac825
commit 76d21900a2
2 changed files with 8 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
library/standard.lean
View file

@ -7,4 +7,4 @@
-- The constructive core of Lean's library.
import logic data tools.tactic
import type logic data tools.tactic

7
library/type.lean Normal file
View file

@ -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}