Dependent typing, refinement types using SMT solver
Testing
Categorize words to specific domain
| import std.array; | |
| import std.stdio; | |
| import std.exception; | |
| import std.string; | |
| import std.conv : to; | |
| import std.algorithm.searching; | |
| import std.algorithm.iteration; | |
| import erupted; | |
| import derelict.sdl2.sdl; |
| Executing task: cargo build < | |
| Compiling shell v0.1.0 (file:///home/swoorup/github/mysh-rs) | |
| error[E0597]: `input` does not live long enough | |
| --> src/main.rs:30:25 | |
| | | |
| 30 | lexer.tokenize(&input); | |
| | ^^^^^ borrowed value does not live long enough | |
| ... | |
| 38 | } |
| module App.View | |
| open Elmish | |
| open Fable.React | |
| open Fable.React.Props | |
| open State | |
| open Types | |
| open Fulma | |
| open Fable.FontAwesome | |
| open Fable.FontAwesome.Free |
| [<AutoOpen>] | |
| module Quantex.Common.Prelude | |
| type Range<'T> = { From: 'T; To: 'T } | |
| module Range = | |
| let create (r: 'T * 'T) = | |
| let (a,b) = r | |
| if (a >= b) then Error("From cannot be greater than To") else Ok({ From = a; To = b}) | |
| type Range<'T> with |
| module Snl.Api.V1.Types where | |
| import Data.Aeson | |
| import Data.Proxy | |
| import Data.Swagger | |
| import Data.Time | |
| import Data.UUID as UUID | |
| import GHC.Generics | |
| import Servant.API | |
| import Snl.Core.Types |
| {-# LANGUAGE NumDecimals #-} | |
| swapNodes :: Int -> [a] -> [a] | |
| swapNodes _ [] = [] | |
| swapNodes k z = swapNodes' z [] | |
| where | |
| swapNodes' [] acc = acc | |
| swapNodes' x acc = | |
| let (a,b) = splitAt k x | |
| firstHalf = if (length a < k) then |
Dependent typing, refinement types using SMT solver
Testing
Categorize words to specific domain
| type private InternalElement<'Key, 'Value when 'Key: comparison> = | |
| { key: 'Key | |
| data: 'Value | |
| polygon: Polygon } | |
| [<Struct>] | |
| type STRtree<'Key, 'Value when 'Key: comparison> = | |
| private { map: Map<'Key, InternalElement<'Key, 'Value>> | |
| strTree: NetTopologySuite.Index.Strtree.STRtree<InternalElement<'Key, 'Value>> } |
| type CompareResult<'a, 'b> = | |
| | FoundPair of 'a * 'b | |
| | UnmatchedLHS of 'a | |
| | UnmatchedRHS of 'b | |
| [<RequireQualifiedAccess>] | |
| module ListCompare = | |
| let compare xsKeySelector ysKeySelector xs ys = | |
| let xs = | |
| xs |
| open System;; | |
| let random = new Random(); | |
| let _rollTheDice (): (int|string) = | |
| let number = random.Next(1, 6) | |
| if (number >= 2) then number else "Winner" | |
| let cls () = System.Console.Clear();; | |
| type A = (int|string|int64) |