|
1 | 1 | (env (dev (flags (:standard -warn-error -A)))) |
2 | 2 |
|
3 | | -(install (files lib/foundations/mltt/proto.anders |
4 | | - lib/foundations/mltt/bool.anders |
5 | | - lib/foundations/mltt/inductive.anders |
6 | | - lib/foundations/mltt/list.anders |
7 | | - lib/foundations/mltt/pi.anders |
8 | | - lib/foundations/mltt/sigma.anders |
9 | | - lib/foundations/univalent/path.anders |
10 | | - lib/foundations/univalent/equiv.anders |
11 | | - lib/foundations/univalent/iso.anders |
12 | | - lib/foundations/modal/infinitesimal.anders |
13 | | - lib/mathematics/algebra/algebra.anders |
14 | | - lib/mathematics/analysis/real.anders |
15 | | - lib/mathematics/analysis/topology.anders |
16 | | - lib/mathematics/categories/category.anders |
17 | | - lib/mathematics/categories/functor.anders |
18 | | - lib/mathematics/categories/abelian.anders |
19 | | - lib/mathematics/categories/groupoid.anders |
20 | | - lib/mathematics/categories/topos.anders |
21 | | - lib/mathematics/geometry/bundle.anders |
22 | | - lib/mathematics/geometry/etale.anders |
23 | | - lib/mathematics/geometry/formalDisc.anders |
24 | | - lib/mathematics/homotopy/coequalizer.anders |
25 | | - lib/mathematics/homotopy/constcubes.anders |
26 | | - lib/mathematics/homotopy/pullback.anders |
27 | | - lib/mathematics/homotopy/pushout.anders |
28 | | - lib/mathematics/homotopy/hubSpokes.anders |
29 | | - lib/mathematics/homotopy/quotient.anders |
30 | | - lib/mathematics/homotopy/truncation.anders |
31 | | - lib/mathematics/homotopy/suspension.anders |
32 | | - lib/mathematics/homotopy/S1.anders |
33 | | - lib/mathematics/homotopy/Sn.anders |
34 | | - lib/mathematics/homotopy/KGn.anders) |
| 3 | +(install (files library/foundations/mltt/proto.anders |
| 4 | + library/foundations/mltt/bool.anders |
| 5 | + library/foundations/mltt/inductive.anders |
| 6 | + library/foundations/mltt/list.anders |
| 7 | + library/foundations/mltt/pi.anders |
| 8 | + library/foundations/mltt/sigma.anders |
| 9 | + library/foundations/univalent/path.anders |
| 10 | + library/foundations/univalent/equiv.anders |
| 11 | + library/foundations/univalent/iso.anders |
| 12 | + library/foundations/modal/infinitesimal.anders |
| 13 | + library/mathematics/algebra/algebra.anders |
| 14 | + library/mathematics/analysis/real.anders |
| 15 | + library/mathematics/analysis/topology.anders |
| 16 | + library/mathematics/categories/category.anders |
| 17 | + library/mathematics/categories/functor.anders |
| 18 | + library/mathematics/categories/abelian.anders |
| 19 | + library/mathematics/categories/groupoid.anders |
| 20 | + library/mathematics/categories/topos.anders |
| 21 | + library/mathematics/geometry/bundle.anders |
| 22 | + library/mathematics/geometry/etale.anders |
| 23 | + library/mathematics/geometry/formalDisc.anders |
| 24 | + library/mathematics/homotopy/coequalizer.anders |
| 25 | + library/mathematics/homotopy/constcubes.anders |
| 26 | + library/mathematics/homotopy/pullback.anders |
| 27 | + library/mathematics/homotopy/pushout.anders |
| 28 | + library/mathematics/homotopy/hubSpokes.anders |
| 29 | + library/mathematics/homotopy/quotient.anders |
| 30 | + library/mathematics/homotopy/truncation.anders |
| 31 | + library/mathematics/homotopy/suspension.anders |
| 32 | + library/mathematics/homotopy/S1.anders |
| 33 | + library/mathematics/homotopy/Sn.anders |
| 34 | + library/mathematics/homotopy/KGn.anders) |
35 | 35 | (section share) (package anders)) |
0 commit comments