Skip to content

A plugin for solving numeric constraints in GHC's type-checker

License

Notifications You must be signed in to change notification settings

yav/type-nat-solver

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 

History

73 Commits
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 

Repository files navigation

SMT-driven typechecking for naturals and booleans

This is a typechecker plugin for GHC using an SMT solver to resolve constraints on booleans and natural numbers.

Usage

Add type-nat-solver to your build-depends list and -fplugin TypeNatSolver to ghc-options.

About

A plugin for solving numeric constraints in GHC's type-checker

Resources

License

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published