File tree 2 files changed +4
-10
lines changed
2 files changed +4
-10
lines changed Original file line number Diff line number Diff line change @@ -162,7 +162,7 @@ rec {
162
162
* Interpretation/evaluation
163
163
*/
164
164
165
- # α-equivalence , M{y,x} (renaming x as y in M)
165
+ # α-renaming , M{y,x} (renaming x as y in M)
166
166
rename = m : y : x :
167
167
if m . type == "var" then m // {
168
168
name = if m . name == x then y else m . name ;
Original file line number Diff line number Diff line change 767
767
}
768
768
769
769
# NOTE: we're indirectly testing again L.parse below ("G"
770
- # is a shortcut calling L.parse, and assuming success)
770
+ # is a shortcut calling L.parse, assuming success)
771
771
{
772
772
descr = ''freeVars "hello"'' ;
773
773
fun = L . freeVars ;
868
868
expected = ( G "y" ) ;
869
869
}
870
870
{
871
- descr = ''rename "(x y) (y z) " y x'' ;
871
+ descr = ''rename "(x y) (y x z) " y x'' ;
872
872
fun = L . rename ;
873
873
args = [ ( G "(x y) (y x z) " ) "y" "x" ] ;
874
874
expected = ( G "(y y) (y y z) " ) ;
892
892
expected = ( G "λz. λy. y z foo bar" ) ;
893
893
}
894
894
{
895
- descr = ''rename "λx. λy. y z foo bar" z x'' ;
896
- fun = L . rename ;
897
- args = [ ( G "λx. λy. y z foo bar" ) "z" "x" ] ;
898
- expected = ( G "λz. λy. y z foo bar" ) ;
899
- }
900
- {
901
- descr = ''rename "λx. λy. y z foo bar" z x'' ;
895
+ descr = ''rename "λx. λy. y z foo bar" foo y'' ;
902
896
fun = L . rename ;
903
897
args = [ ( G "λx. λy. y z foo bar" ) "foo" "y" ] ;
904
898
expected = ( G "λx. λfoo. foo z foo bar" ) ;
You can’t perform that action at this time.
0 commit comments