diff options
| author |  Jade Philipoom <jadep@mit.edu> | 2016-03-20 17:09:44 -0400 |
|---|---|---|
| committer | Jade Philipoom <jadep@mit.edu> | 2016-03-20 17:09:44 -0400 |
| commit | dc51191d484348bf827f91fd4ee5dd088fd5e17b (patch) | |
| tree | efcec532cdb798e77841bd9503493109ff9892c6 /src/BaseSystem.v | |
| parent | 2f178e16ab2e44b6139ef01dca17f425f02bb319 (diff) | |
made BaseVector instance global
Diffstat (limited to 'src/BaseSystem.v')
| -rw-r--r-- | src/BaseSystem.v | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/src/BaseSystem.v b/src/BaseSystem.v index f3a1a0fdb..627550440 100644 --- a/src/BaseSystem.v +++ b/src/BaseSystem.v @@ -85,6 +85,7 @@ Section BaseSystem. End BaseSystem. +(* Example : polynomial base system *) Section PolynomialBaseCoefs. Context (b1 : positive) (baseLength : nat) (baseLengthNonzero : NPeano.ltb 0 baseLength = true). (** PolynomialBaseCoefs generates base vectors for [BaseSystem]. *) |