kdrag.theories.logic.computable

Module Attributes

mu	//isabelle.in.tum.de/library/HOL/HOL-Library/Countable_Set.html f = smt.Function("f", smt.IntSort(), A) countable = kd.define( "countable", [A], smt.Exists([f], smt.ForAll([x], smt.Exists[m]) )"

kdrag.theories.logic.computable.mu = mu

//isabelle.in.tum.de/library/HOL/HOL-Library/Countable_Set.html f = smt.Function(“f”, smt.IntSort(), A) countable = kd.define(

“countable”, [A], smt.Exists([f], smt.ForAll([x], smt.Exists[m])

)”

SKI combinators

Krivine Machine

Type:

# https