معرفی

اثبات چک کن یک proof assisstan است مانند coq ولی با قابلیت های کمتری که برای نوشتن گزاره ها در coq پیاده سازی شده است ولی از نظر ui با کاربر چون از گرافیک خوبی برخوردار است مزیت بسزایی دارد.

#ترم چیست?

ترم یک عبارت مشابه term در زبان coq است که در type theory برای نمایش اشیا ریاضی استفاده می شود.

ترم ها همشه تایپ دارند چند ترم پایه که در سیستم معرفی می کنیم

• Universe

این ترم مانند Type در coq است و ویژگی های Type را دارد یعنی تایپ آن خودش است البته با یک index بیشتر چون این ترم یک عدد را به عنوان index پنهان می کند.

• ℤ

این ترم برای اعداد صحیح بیان می شود و تایپ آن Universe است.

این ترم برای نمایش تایپ هر عددی، متغیر آزادی، یا هر عبارتی استفاده می شود چند مثال زیر چند شی را بیان می کند که تایپ آنها ℤ است .

برای نمایش اینکه تایپ ترم A ترم B است از A: B استفاده می کنیم.

2: ℤ

-1000: ℤ

(در کل هر عددی که ممیز نداشته باشد یک ترم با تایپ ℤ است)

x: ℤ

(هر اسم آزادی)

2 + 3: ℤ

2 + x: ℤ

جمع هر دوتا ترمی که تایپ آنها از ℤ باشد نیز تایپش ℤ است.

نکته: جمع یک binary oprator است که دو ترم از یک نوع را در دو سمت خود ورودی می گیرد و خود یک ترم تشکیل می دهذ.

2 * x: ℤ

x * x: ℤ

ضرب هردوتا ترمی که تایپ آنها ℤ باشد نیز تایپش ℤ است.

ضرب نیست خواض جمع را دارد.