proj-jasper-jasperToReads

see also [1]

toreads

link Try adding a language with proof solving capabilities. ATS, Agda, Idris, Coq spring to mind.
  1. The base environment for an Ur-Lisp written in Ruby @env = { :label => proc {
(name,val), _@env[name] = eval(val, @env) },
 :car   => lambda { |(list), _| list[0] },
 :cdr   => lambda { |(list), _| list.drop 1 },
 :cons  => lambda { |(e,cell), _| [e] + cell },
 :eq    => lambda { |(l,r),ctx| eval(l, ctx) == eval(r, ctx) },
 :if    => proc { |(c,t,e),ctx| eval(c, ctx) ? eval(t, ctx) : eval(e, ctx) },
 :atom  => lambda { |(s), _| (s.is_a? Symbol) or (s.is_a? Numeric) },
 :quote => proc { |sexpr, _| sexpr[0] } }"