Skip to content

This a type-checker plugin to rule all type checker plugins involving type-equality reasoning using smt solvers.

License

Notifications You must be signed in to change notification settings

bgamari/the-thoralf-plugin

Repository files navigation

the-thoralf-plugin

Build Status

This a type-checker plugin for type-indicies such as type level natural numbers and type level finite maps.

Setup

You need

To build simply

$ git clone [email protected]:Divesh-Otwani/the-thoralf-plugin.git
$ cd the-thoralf-plugin
$ stack install
$ echo "Now the example should load or run!"
$ stack ghci test/Main.hs

Loaded GHCi configuration from /home/divesh/.ghc/ghci.conf
[1 of 1] Compiling Main             ( test/Main.hs, interpreted )
Ok, 1 module loaded.
*Main> 

Usage

  • See DOCUMENTATION.md for how to extend thoralf and make your own plugin with all of thoralf's theories and some new ones you write.

About

This a type-checker plugin to rule all type checker plugins involving type-equality reasoning using smt solvers.

Topics

Resources

License

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published

Contributors 4

  •  
  •  
  •  
  •