Agda (programming language)

خطای اسکریپتی: پودمان «AfC submission catcheck» وجود ندارد.

ین مقاله در حال ترجمه از ویکی انگلیسی است لطفا حذف نشودهمچنین یک دستیار اثبات مبتنی بر پارادایم گزاره‌ها به‌عنوان انواع است ، اما برخلاف Coq ، زبان تاکتیکی جداگانه‌ای ندارد و اثبات‌ها به سبک برنامه‌نویسی تابعی نوشته می‌شوند. این زبان دارای ساختارهای برنامه نویسی معمولی مانند انواع داده ، تطبیق الگو ، رکوردها ، عبارات و ماژول‌های let، و نحوی شبیه به Haskell است. این سیستم دارای رابط های Emacs و Atom ^[۱] اما می تواند در حالت دسته ای از خط فرمان نیز اجرا شود.

این روش نوشتن توابع بازگشتی/ اثبات های استقرایی طبیعی تر از اعمال اصول القایی خام است. در Agda، تطبیق الگوی تایپ شده وابسته، ابتدایی زبان است. زبان اصلی فاقد اصول استقرا/بازگشت است که تطبیق الگو به آن ترجمه می شود. رده:نرم‌افزارهای سال ۲۰۰۷ (میلادی) رده:زبان‌های برنامه‌نویسی ساخته‌شده در ۲۰۰۷ (میلادی) رده:دانشگاه صنعتی چالمرز رده:کامپایلرها و مفسرهای آزاد رده:نرم‌افزارهای آزاد چندسکویی رده:دستیارهای اثباتی رده:زبان‌های برنامه‌نویسی ایستا رده:زبان‌های برنامه‌نویسی آکادمیک رده:زبان‌های برنامه‌نویسی تطبیق الگو رده:زبان‌های تابعی رده:زبان‌های برنامه‌نویسی

This article "Agda (programming language)" is from Wikipedia. The list of its authors can be seen in its historical and/or the page Edithistory:Agda (programming language). Articles copied from Draft Namespace on Wikipedia could be seen on the Draft Namespace of Wikipedia and not main one.