lean2/library/standard/unit.lean

-- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
-- Released under Apache 2.0 license as described in the file LICENSE.
-- Author: Leonardo de Moura
import logic

inductive unit : Type :=
| tt : unit

theorem inhabited_unit [instance] : inhabited unit
:= inhabited_intro tt
chore(library/standard): add copyright to library files Signed-off-by: Leonardo de Moura <leonardo@microsoft.com> 2014-06-30 18:44:47 +00:00			`-- Copyright (c) 2014 Microsoft Corporation. All rights reserved.`
			`-- Released under Apache 2.0 license as described in the file LICENSE.`
			`-- Author: Leonardo de Moura`
feat(library/standard): add inhabited, and files option and unit Signed-off-by: Leonardo de Moura <leonardo@microsoft.com> 2014-06-30 02:30:38 +00:00			`import logic`

			`inductive unit : Type :=`
			`\| tt : unit`

feat(frontends/lean): add 'class' and 'instances' infrastructure Signed-off-by: Leonardo de Moura <leonardo@microsoft.com> 2014-07-04 21:25:44 +00:00			`theorem inhabited_unit [instance] : inhabited unit`
feat(library/standard): add inhabited, and files option and unit Signed-off-by: Leonardo de Moura <leonardo@microsoft.com> 2014-06-30 02:30:38 +00:00			`:= inhabited_intro tt`