내부 구문 주석 내부의 큰 따옴표

Question

" 문자는 큰 따옴표로 묶인 Isabelle의 내부 구문에 주석 안에 넣을 때 예상대로 동작하지 않습니다. 명확히하기 위해 : 다음 함수 정의에서, 나는 the "at" sign이 주석으로 해석 될 것으로 기대한다. 실제로 Isabelle은 주석의 첫 번째 " 문자를 해당 라인의 시작 부분 인 "과 일치 시키므로 구문 오류가 발생합니다.

fun reverse where 
    "reverse [] = []" 
| "reverse (x#xs) = reverse xs @ (* the "at" sign *) [x]" 

내가 (* the 'at' sign *)를 작성하여이 문제를 해결 할 수 있습니다,하지만 난 오히려 정말 무슨 일이 일어나고 있는지 이해하는 것입니다. 그렇다면 이사벨 (Isabelle) 용어에 이런 종류의 주석을 쓰는 올바른 방법은 무엇입니까? 나는 그것이 \ "같은 이스케이프 문자와 함께 일하는 것이 가정

Answer 1

?

이