maude-help AT lists.cs.illinois.edu

Subject: Maude-help mailing list

List archive

[[maude-help] ] understanding lack of error when types are mismatched

From: Raghu Ranganathan <rraghu.11502 AT gmail.com>
To: maude-help AT lists.cs.illinois.edu
Subject: [[maude-help] ] understanding lack of error when types are mismatched
Date: Fri, 8 Dec 2023 06:39:53 +0800

fmod LIST-OPS{X :: TRIV} is
pr LIST*{X} .
var A : X$Elt .
var B : Nat .
var C : List{X} .

op index : List{X} Nat -> X$Elt .
eq index(A,0) = head(A) .
eq index(A,s B) = index(tail(A),B) .
endfm

fmod LIST-TEST is pr LIST-OPS{Nat} . endfm

This is the code i have, the strange portion is how A is of kind X$Elt but still is allowed to compile

as an argument in the equation for index. I am wondering how to detect these bugs when they happen.

[[maude-help] ] understanding lack of error when types are mismatched, Raghu Ranganathan, 12/07/2023
- Re: [[maude-help] ] understanding lack of error when types are mismatched, Steven Eker, 12/07/2023