<jupyter_start><jupyter_text>Sylvester.Arithmetic IntroductionThis [library](https://github.com/allisterb/Sylvester/tree/master/src/Base/Sylvester.FixedPoint) implements [lightweight](http://okmij.org/ftp/Computation/lightweight-dependent-typing.html) dependently typed natural number arithmetic and constraints in F which enable arithmetic operations like bounds checking to be performed at compile-time by the F type checker as long as the values for the operations are known at compile-time.<jupyter_code>/// Use the Sylvester.Arithmetic NuGet package in this notebook// Use the Sylvester arithmetic and collection packages
# r "nuget:Sylvester.Arithmetic"

open Sylvester.Arithmetic
open Sylvester.Arithmetic.N10

///Create typed representations of some natural numbers
let a,b,c = new n<400>(), new n<231111>(), new n<6577700>()

a + b + c<jupyter_output><empty_output><jupyter_text>These values have types derived from *Sylvester.Arithmetic.N10*. The type of ``a`` is *N10* and the type of ``c`` is *N10*.<jupyter_code>c.GetType()<jupyter_output><empty_output><jupyter_text>The types of the results of arithmetic operations depend on the values of the operands.<jupyter_code>let d = (a + b + c) * four

d
d.GetType()<jupyter_output><empty_output><jupyter_text>This enables type-level constraints to be written which run at compile-time<jupyter_code>N<4>.i +== four ///Compare two instances of N<4>
///Type level comparison operators return types dependent on the result of the comparison
N<4>.i +== thousand
/// The check functions performs type level checks. 
check(d +< ten) ///This check causes a type error at compile time
a - (two * a) /// A negative number results in a type representing an underflow at compile-time 
/// Define a function myop using type-level arithmetic constraintss
let myop a b c d =
    check(a +> b) /// Use the +> and +< operators for type-level comparisons
    check (b +== zero) /// +== Type level equality operator
    check (c +== (a + one))
    a + b + c + d
    
/// Call the function with values that don't satisfy the constraints 
/// This will cause a type error and the code won't compile
myop four N<1000>.i three two 
let myop a b c d =
    check(a +> b)
    check (b +== zero)
    check (c +== (a + one))
    a + b + c + d
    
/// This call to myop satisfies the arithmetic constraints so the code compiles
myop five zero six N<10>.i<jupyter_output><empty_output><jupyter_text>Mixing natural number and primitive types result in the natural numbers being lowered to their primitive representation.<jupyter_code>seven + eight
seven + eight + 1<jupyter_output><empty_output>
{'fraction_non_alphanumeric': 0.10106788710907703, 'fraction_numerical': 0.012967200610221205, 'mean_word_length': 4.375, 'pattern_counts': {'":': 0, '<': 31, '<?xml version=': 0, '>': 32, 'https://': 1, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'chain_length': '5', 'dir': 'jupyter-structured-clean-dedup', 'id': '96794', 'license': 'MIT', 'n_tokens_mistral': 831, 'n_tokens_neox': 776, 'n_words': 306, 'path': 'notebooks/Sylvester.Arithmetic.ipynb', 'repo_name': 'allisterb/Sylvester', 'size': '2622'}