ACGtk issueshttps://gitlab.inria.fr/ACG/dev/ACGtk/-/issues2023-10-06T11:30:11+02:00https://gitlab.inria.fr/ACG/dev/ACGtk/-/issues/42using `-s` parameter for `acg` in combination with `|`2023-10-06T11:30:11+02:00POGODALLA Sylvainusing `-s` parameter for `acg` in combination with `|``cat montague-script | acg` works fine, but `cat montague-script | acg -s` raises (uncaught) exceptions.
The same holds for `ls montague-script | xargs -n 1 acg` and `ls montague-script | xargs -n 1 acg -c`.`cat montague-script | acg` works fine, but `cat montague-script | acg -s` raises (uncaught) exceptions.
The same holds for `ls montague-script | xargs -n 1 acg` and `ls montague-script | xargs -n 1 acg -c`.Vincent TourneurVincent Tourneurhttps://gitlab.inria.fr/ACG/dev/ACGtk/-/issues/16Parametrize "show" so that only the root of tree showing the combination is s...2018-10-05T12:11:38+02:00POGODALLA SylvainParametrize "show" so that only the root of tree showing the combination is shownParametrize "show" so that only the root of the tree showing the derivation is shown.Parametrize "show" so that only the root of the tree showing the derivation is shown.POGODALLA SylvainPOGODALLA Sylvainhttps://gitlab.inria.fr/ACG/dev/ACGtk/-/issues/10"This term is not in normal form" ; so what ?2018-07-05T10:39:40+02:00LUDMANN Pierre"This term is not in normal form" ; so what ?Hi,
I don't understand why the following refuse to compile.
```acg
signature TMP =
a : type ;
M, N : a ;
t = (Lambda x. M) N : a ;
end
```
I sure understand the error message "This term is not in normal form". But then why t...Hi,
I don't understand why the following refuse to compile.
```acg
signature TMP =
a : type ;
M, N : a ;
t = (Lambda x. M) N : a ;
end
```
I sure understand the error message "This term is not in normal form". But then why the following compiles?
```acg
signature TMP =
a : type ;
M, N : a ;
u = (Lambda x. M) : a => a ;
t = u N : a ;
end
```
Besides, assume N is not a value yet and will only become so through epsilon-reductions. ACGtk doesn't account for such reductions — which may be for the best. Then the first `t` __is__ in normal form w.r.t. beta-eta-reductions. This hypothetical case is how I stumble on that issue.
Please free us from that normative straightjacket!