Skip to content

A fuelled self-reducer for System T, embedded in Idris 2

Notifications You must be signed in to change notification settings

yellowsquid/syst-reducer

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 

History

28 Commits
 
 
 
 
 
 
 
 

Repository files navigation

System T Self-Reducer

A fuelled self-reducer for System T embedded in Idris 2

Code Structure

  • Term.idr :: Deep embedding of System T terms, using co-deBruijn variable bindings.
  • Term/Syntax.idr :: Smart constructors for System T terms, doing some simplification.
  • Encodings/ :: Encodings of various types.

About

A fuelled self-reducer for System T, embedded in Idris 2

Resources

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published

Languages