chore(library/standard): add copyright to library files
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
parent
cb000eda13
commit
15e4b18d62
3 changed files with 9 additions and 0 deletions
|
@ -1,3 +1,6 @@
|
|||
-- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
|
||||
-- Released under Apache 2.0 license as described in the file LICENSE.
|
||||
-- Author: Leonardo de Moura
|
||||
definition Bool [inline] := Type.{0}
|
||||
|
||||
inductive false : Bool :=
|
||||
|
|
|
@ -1,3 +1,6 @@
|
|||
-- 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 option (A : Type) : Type :=
|
||||
|
|
|
@ -1,3 +1,6 @@
|
|||
-- 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 :=
|
||||
|
|
Loading…
Reference in a new issue