15 lines
347 B
Plaintext
15 lines
347 B
Plaintext
module sec9_2
|
|
imports prop-eval2 prop-desugar
|
|
|
|
rules
|
|
DefT : True() -> Impl(False(), False())
|
|
|
|
strategies
|
|
eval1 = bottomup(try(Eval))
|
|
eval2 = topdown(try(Eval))
|
|
|
|
desugar2 = bottomup(try(DefI <+ DefE))
|
|
|
|
impl-nf1 = topdown(repeat(DefT <+ DefN <+ DefA2 <+ DefO1 <+ DefE))
|
|
impl-nf2 = topdown(try(DefT <+ DefN <+ DefA2 <+ DefO1 <+ DefE))
|