diff options
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]. *) |