짧은 ::
(1.) "Coq"는 수학 읽기와 쓰기를위한 컴퓨터 프로그램입니다 .
(2.) 유한 이진 데이터는 다음과 같습니다. 참된 ; 그릇된 .
(3.) 무한한 숫자는 이것들입니다. 0 ; 1 = 0 다음 ; 2 = 1 다음 ; 3 = 2 다음 ; 4 = 3 다음 .
(4.) 항목이 포함 된 무한한 목록은 다음과 같을 수 있습니다. [ ] ; [ 고양이 ] ; [ 개, 고양이 ] ; [ 물고기, 개, 고양이 ] ...
다른 예시 : [ ] ; [ 레드 ] ; [ 파랑 , 빨강 ] ; [ 금 , 파랑 , 빨강 ]; [ 녹색 , 금색 , 파란색 , 빨간색 ] ...
이것은 "다형성"이라고 부릅니다.
(5.) 이 표기법 [ "X", "Y", "Z"]은이 항목 "X", "Y", "Z"의 유형/양식을 숨 깁니다.
예를 들어이 숨겨진 데이터 유형은 동물이나 색상 일 수 있습니다.
이 숨겨진/암시 적 데이터 유형을 유추 할 수 있습니다.
이것은 "암시 적 표기법"이라고합니다.

Short ::
(1.) "Coq" is computer program to read and write mathematics .
(2.) The finite binary data are these : true ; false .
(3.) The infinite numbers are these : 0 ; 1 = next after 0 ; 2 = next after 1 ; 3 = next after 2 ; 4 = next after 3 ; ...
(4.) The infinite lists which contain items can be these : [ ] ; [ cat ] ; [ dog , cat ] ; [ fish , dog , cat ] ...
Another example : [ ] ; [ red ] ; [ blue , red ] ; [ gold , blue , red ] ; ; [ green , gold , blue , red ] ...
This is named "polymorphism" .
(5.) This notation [ "X" , "Y" , "Z" ] hides the type/form of these items "X" , "Y" , "Z" .
For example , this hidden data-type could be animals or colors .
This hidden/implicit data-type can be inferred .
This is named "implicit notation" .

Alt+↑/↓ – move through proof; Alt+→ or Alt+⏎ – go to cursor.
Alt+hover executed sentences to watch intermediate steps.
Hover identifiers in goals to view their types. Alt+hover to view definitions.
Company-coq addon is enabled: it will auto-complete names of tactics and lemmas from the standard library, and also show types of lemmas in the right pane.

"Alt + ↑ / ↓": 증명을 전달하십시오. "Alt + →"또는 "Alt + ⏎": 커서로 이동하십시오.
"Alt +"호버링은 문장을 실행하여 중간 단계를 관찰합니다.
대상에 식별자를 올려 해당 유형을 표시합니다. "Alt +"를 가리키면 정의를 볼 수 있습니다.
"Company-coq"애드온을 활성화하십시오 : 표준 라이브러리의 정책 및 보조 정리 이름을 자동으로 완성하고 오른쪽 창에 부트 유형을 표시하십시오.

From Qoc Require Import Sutalgsuhag . (** 1짧은 :: (1.) "Coq"는 수학 읽기와 쓰기를위한 컴퓨터 프로그램입니다 . (2.) 유한 이진 데이터는 다음과 같습니다. 참된 ; 그릇된 . (3.) 무한한 숫자는 이것들입니다. 0 ; 1 = 0 다음 ; 2 = 1 다음 ; 3 = 2 다음 ; 4 = 3 다음 . (4.) 항목이 포함 된 무한한 목록은 다음과 같을 수 있습니다. [ ] ; [ 고양이 ] ; [ 개, 고양이 ] ; [ 물고기, 개, 고양이 ] ... 다른 예시 : [ ] ; [ 레드 ] ; [ 파랑 , 빨강 ] ; [ 금 , 파랑 , 빨강 ]; [ 녹색 , 금색 , 파란색 , 빨간색 ] ... 이것은 "다형성"이라고 부릅니다. (5.) 이 표기법 [ "X", "Y", "Z"]은이 항목 "X", "Y", "Z"의 유형/양식을 숨 깁니다. 예를 들어이 숨겨진 데이터 유형은 동물이나 색상 일 수 있습니다. 이 숨겨진/암시 적 데이터 유형을 유추 할 수 있습니다. 이것은 "암시 적 표기법"이라고합니다. Short :: (1.) "Coq" is computer program to read and write mathematics . (2.) The finite binary data are these : true ; false . (3.) The infinite numbers are these : 0 ; 1 = next after 0 ; 2 = next after 1 ; 3 = next after 2 ; 4 = next after 3 ; ... (4.) The infinite lists which contain items can be these : [ ] ; [ cat ] ; [ dog , cat ] ; [ fish , dog , cat ] ... Another example : [ ] ; [ red ] ; [ blue , red ] ; [ gold , blue , red ] ; ; [ green , gold , blue , red ] ... This is named "polymorphism" . (5.) This notation [ "X" , "Y" , "Z" ] hides the type/form of these items "X" , "Y" , "Z" . For example , this hidden data-type could be animals or colors . This hidden/implicit data-type can be inferred . This is named "implicit notation" . *) 꾸러미 다형'유도성'암시적인'표기법 . 유도성 목록'다형 (데이터 : 종류) : 종류 := 빈 : 목록'다형 데이터 | 합류한다'하나의 : 기능 (d : 데이터) (l : 목록'다형 데이터), 목록'다형 데이터. 정의 나머지에서_목록'다형 : 기능 (데이터 : 종류) (l : 목록'다형 데이터), 목록'다형 데이터 . 증명 . 이동해'밖 데이터 l . 파괴해라 l 로 [ | dat l' ] . - 정확하다 (빈 데이터) . - 정확하다 l' . 정의된 . 유도성 이진 : 종류 := 참된 : 이진 | 그릇된 : 이진 . 계산해라 (나머지에서_목록'다형 이진 (합류한다'하나의 이진 그릇된 (합류한다'하나의 이진 그릇된 (합류한다'하나의 이진 참된 (빈 이진))))) . 유도성 무한'수들 : 종류 := 제로 : 무한'수들 | 다음한 : 무한'수들 -> 무한'수들 . 계산해라 (나머지에서_목록'다형 무한'수들 (합류한다'하나의 무한'수들 (다음한 (다음한 제로)) (합류한다'하나의 무한'수들 제로 (합류한다'하나의 무한'수들 (다음한 제로) (빈 무한'수들))))) . 계산해라 (합류한다'하나의 이진 참된 (빈 이진)). 계산해라 (합류한다'하나의 _ 참된 (빈 _)). 계산해라 (합류한다'하나의 _ (다음한 (다음한 제로)) (빈 _)). (**MEMO: polymorphism-objects can be inferred-implicit , via [표기법] command *) 표기법 "d :: l" := (합류한다'하나의 _ d l) . 표기법 "!00!" := (빈 _) . 계산해라 ( 참된 :: !00! ). 계산해라 ( (다음한 (다음한 제로)) :: !00! ). 계산해라 (나머지에서_목록'다형 _ ( 그릇된 :: 그릇된 :: 참된 :: !00! ) ) . 계산해라 (나머지에서_목록'다형 _ ( (다음한 (다음한 제로)) :: 제로 :: (다음한 제로) :: !00! ) ) . 표기법 "'나머지'" := ( 나머지에서_목록'다형 _ ) . 계산해라 (나머지 ( 그릇된 :: 그릇된 :: 참된 :: !00! ) ) . (**MEMO: polymorphism-objects can be inferred-implicit , via [입력들] command *) 입력들 나머지에서_목록'다형 [데이터] l . 계산해라 (나머지에서_목록'다형 ( 그릇된 :: 그릇된 :: 참된 :: !00! ) ) . 부분 부분_다형 . 변수 데이터 : 종류 . (** the precise form/type of the output ( precisely [unit] or [데이터] ? ) depends on the input *) 유도성 옵션'다형 : 종류 := 입력_유효하지'않은 : (* unit -> *) 옵션'다형 | 입력_유효한 : 데이터 -> 옵션'다형 . 끝 부분_다형 . 인쇄해 옵션'다형 . 인쇄해 unit . 설정해라 암시적인 입력들 . (** in some sense , the precise form/type of the output ( precisely [unit] or [데이터] ? ) depends on the (parameter of the) input ( whether [l] is invalid or valid ? ) *) 정의 상단에서_목록'다형 : 기능 (데이터 : 종류) (l : 목록'다형 데이터), 옵션'다형 데이터. 증명 . 이동해'밖 데이터 l . 경우 l . - 정확하다 (입력_유효하지'않은 데이터). - 이동해'밖 dat l' . 적용해라 (입력_유효한 데이터) . 정확하다 dat . 정의된 . 계산해라 (상단에서_목록'다형 ( 그릇된 :: 그릇된 :: 참된 :: !00! ) ) . 고정점 바닥에서_목록'다형 (데이터 : 종류) (l : 목록'다형 데이터) {구조 l} : 옵션'다형 데이터 . 증명 . 파괴해라 l 로 [ | dat l' ] . - 정확하다 (입력_유효하지'않은 데이터) . - 경우 (바닥에서_목록'다형 데이터 l') . + 정확하다 (입력_유효한 데이터 dat). + 지우해라 l' . 이동해'밖 바닥에서_목록'다형_데이터_l' . 적용해라 (입력_유효한 데이터). 정확하다 바닥에서_목록'다형_데이터_l' . 정의된 . 계산해라 (바닥에서_목록'다형 ( 그릇된 :: 그릇된 :: 참된 :: !00! )) . 끝 다형'유도성'암시적인'표기법 . (** ** alt ----------------------------------------------------------------------------- *) Modular PolymorphismInductiveImplicitNotations . Inductive listPoly (data : Type) : Type := Empty : listPoly data | JoinOne : forall (d : data) (l : listPoly data), listPoly data. Definition rest_of_listPoly : forall (data : Type) (l : listPoly data), listPoly data . Proof . intros data l . destruct l as [ | dat l' ] . - exact (Empty data) . - exact l' . Defined . Inductive binary : Type := true : binary | false : binary . Compute (rest_of_listPoly binary (JoinOne binary false (JoinOne binary false (JoinOne binary true (Empty binary))))) . Inductive infiniteNumbers : Type := Zero : infiniteNumbers | NextOne : infiniteNumbers -> infiniteNumbers . Compute (rest_of_listPoly infiniteNumbers (JoinOne infiniteNumbers (NextOne (NextOne Zero)) (JoinOne infiniteNumbers Zero (JoinOne infiniteNumbers (NextOne Zero) (Empty infiniteNumbers))))) . Compute (JoinOne binary true (Empty binary)). Compute (JoinOne _ true (Empty _)). Compute (JoinOne _ (NextOne (NextOne Zero)) (Empty _)). (**MEMO: polymorphism-objects can be inferred-implicit , via [Notation] command *) Notation "d :: l" := (JoinOne _ d l) . Notation "!00!" := (Empty _) . Compute ( true :: !00! ). Compute ( (NextOne (NextOne Zero)) :: !00! ). Compute (rest_of_listPoly _ ( false :: false :: true :: !00! ) ) . Compute (rest_of_listPoly _ ( (NextOne (NextOne Zero)) :: Zero :: (NextOne Zero) :: !00! ) ) . Notation "'rest'" := ( rest_of_listPoly _ ) . Compute (rest ( false :: false :: true :: !00! ) ) . (**MEMO: polymorphism-objects can be inferred-implicit , via [Arguments] command *) Arguments rest_of_listPoly [data] l . Compute (rest_of_listPoly ( false :: false :: true :: !00! ) ) . Section section_polymorphism . Variable data : Type . (** the precise form/type of the output ( precisely [unit] or [data] ? ) depends on the input *) Inductive optionPoly : Type := Input_Invalid : (* unit -> *) optionPoly | Input_Valid : data -> optionPoly . End section_polymorphism . Print optionPoly . Print unit . Set Implicit Arguments . (** in some sense , the precise form/type of the output ( precisely [unit] or [data] ? ) depends on the (parameter of the) input ( whether [l] is invalid or valid ? ) *) Definition top_of_listPoly : forall (data : Type) (l : listPoly data), optionPoly data. Proof . intros data l . case l . - exact (Input_Invalid data). - intros dat l' . apply (Input_Valid data) . exact dat . Defined . Compute (top_of_listPoly ( false :: false :: true :: !00! ) ) . Fixpoint bottom_of_listPoly (data : Type) (l : listPoly data) {struct l} : optionPoly data . Proof . destruct l as [ | dat l' ] . - exact (Input_Invalid data) . - case (bottom_of_listPoly data l') . + exact (Input_Valid data dat). + clear l' . intros bottom_of_listPoly_data_l' . apply (Input_Valid data). exact bottom_of_listPoly_data_l' . Defined . Compute (bottom_of_listPoly ( false :: false :: true :: !00! )) . End PolymorphismInductiveImplicitNotations .