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

feat(library/data/default.lean): add rat and vector

Browse source
This commit is contained in:
Jeremy Avigad 2015-05-17 12:19:47 +10:00
parent ff701a9812
commit 981bf93ce0
1 changed files with 2 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
library/data/default.lean
View file

@ -1,9 +1,7 @@
/-
Copyright (c) 2014 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Module: data.default
Author: Jeremy Avigad
-/
import .empty .unit .bool .num .string .nat .int .fintype
import .prod .sum .sigma .option .subtype .quotient .list .finset .set
import .empty .unit .bool .num .string .nat .int .rat .fintype
import .prod .sum .sigma .option .subtype .quotient .list .vector .finset .set