acl2 / acl2/acl2

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

Offen
#445 0 Kommentare 0 Reaktionen 0 zugewiesene Personen Auf GitHub ansehen
Component: FTY
Vorherrschende Sprache
Common Lisp
Sterne
447
Forks
127
Ø Merge
22 Std. 44 Min.
Gemergte PRs (30 T.)
18

Beschreibung

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.

Beitragsleitfaden

Für dieses Repository ist kein Beitragsleitfaden indexiert

Bewertung

Dieses Issue wurde noch nicht bewertet.

Neue Issues direkt in Ihr Postfach

Eine kurze Übersicht über anfängerfreundliche GitHub-Issues.