-
Notifications
You must be signed in to change notification settings - Fork 3
Open
Description
I have the following code:
// Part D: formulate and prove the associativity of or, namely
// that (X || Y) || Z and X || (Y || Z) are equivalent / the same
absprop PEQ (A: prop, B: prop)
propdef <->(A: prop, B: prop) = PEQ(A, B)
extern praxi peq_intro {A, B: prop}: (A ->> B) && (B ->> A) -> (A <-> B)
extern praxi peq_elim_from_right {A, B: prop}: (A <-> B) -> B -> A
extern praxi peq_elim_from_left {A, B: prop}: (A <-> B) -> A -> B
And when I try to run acc as follow:
NAME = logic
build: $(NAME).dats
acc pc -o $(NAME) $(NAME).dats
I got the following error message:
acc pc -o logic logic.dats
/mnt/c/Users/zcsxo/githubRepos/CS591K1-Labs/homework3/Problem1/logic.dats: 123:49-50
123| extern praxi peq_elim_from_right {A, B: prop}: (A <-> B) -> B -> A
^
error: the static expression
A(4324)
/mnt/c/Users/zcsxo/githubRepos/CS591K1-Labs/homework3/Problem1/logic.dats: 124:48-49
124| extern praxi peq_elim_from_left {A, B: prop}: (A <-> B) -> A -> B
^
error: the static expression
A(4326)
patsopt(TRANS2): there are [2] errors in total.
exit(ATS): (1025)
Makefile:4: recipe for target 'build' failed
make: *** [build] Error 1
which is not that helpful.
When I run the vanilla compiler:
ugly: $(NAME).dats
patscc -o $(NAME) $(NAME).dats
I get the following message:
patscc -o logic logic.dats
/mnt/c/Users/zcsxo/githubRepos/CS591K1-Labs/homework3/Problem1/logic.dats: 4330(line=123, offs=49) -- 4331(line=123, offs=50): error(2): the static expression [S2Evar(A(4324))] is expected to be of a functional sort but it is assigned the sort [S2RTbas(S2RTBASimp(5; prop))].
/mnt/c/Users/zcsxo/githubRepos/CS591K1-Labs/homework3/Problem1/logic.dats: 4398(line=124, offs=48) -- 4399(line=124, offs=49): error(2): the static expression [S2Evar(A(4326))] is expected to be of a functional sort but it is assigned the sort [S2RTbas(S2RTBASimp(5; prop))].
patsopt(TRANS2): there are [2] errors in total.
exit(ATS): uncaught exception: _2mnt_2c_2tools_2ATS2_2src_2pats_error_2esats__FatalErrorExn(1025)
Makefile:7: recipe for target 'ugly' failed
make: *** [ugly] Error 1
Metadata
Metadata
Assignees
Labels
No labels