SF

Coq implementation of SF-calculus and the tranlsation to it of lift lambda-calculus

Name		Name	Last commit message	Last commit date
Latest commit History 6 Commits
Lift		Lift
Equal.v		Equal.v
Eval.v		Eval.v
Extensions.v		Extensions.v
General.v		General.v
LICENSE		LICENSE
Lifting.v		Lifting.v
README.md		README.md
SF_Closed.v		SF_Closed.v
SF_Eval.v		SF_Eval.v
SF_Normal.v		SF_Normal.v
SF_Tactics.v		SF_Tactics.v
SF_Terms.v		SF_Terms.v
SF_arithmetic.v		SF_arithmetic.v
SF_reduction.v		SF_reduction.v
Star.v		Star.v
Substituting.v		Substituting.v
Substitution_term.v		Substitution_term.v
Test.v		Test.v
script		script
substitution_combinator.pdf		substitution_combinator.pdf

Provide feedback