acl2 / acl2/acl2

[fty] deftagsum error not as clear as it could be

Aperta
#445 0 commenti 0 reazioni 0 assegnatari Vedi su GitHub
Component: FTY
Lingua principale
Common Lisp
Stelle
447
Fork
127
Merge medio
22h 44m
PR unite (30g)
18

Descrizione

The following error is a bit misleading. It'd be clearer to say that venue-p doesn't have a definition.

```
HARD ACL2 ERROR in FTY::GET-TYPE-AND-FIX: Type VENUE-P doesn't have
an associated fixing function. Please provide that association using
FTY::DEFFIXTYPE.
```

The code to generate the error:

```
(include-book "std/top" :dir :system)
(include-book "centaur/fty/deftypes" :dir :system)

(std::defenum venue
(:stadium :convention-center :outdoors))

(fty::deftagsum sport
(:blurnball ((venue venue-p)))
(:golf ((venue venue-p)))
(:basketball ((venue venue-p)))
(:chess ())) ; no venue
```

I'm leaving unassigned -- I assume I can fix this pretty easily at some point.

Guida per i contributori

Nessuna guida per i contributori indicizzata per questo repository

Valutazione

Questa issue non è ancora stata valutata.

Ricevi le nuove issue nella tua casella

Un breve riepilogo di issue GitHub adatte ai principianti.