This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
(* Context와 state가 있는 프로그래밍 언어를 정형화하고자 합니다. | |
프로그래밍 변수로는 De Brujin index를 사용할 것이며, | |
따라서 context는 단순히 데이터 타입들의 리스트 입니다. | |
(예를 들어서 int :: int :: boolean :: nil 이 하나의 context입니다. | |
리스트를 사용해서 생기는 문제를 해결해 봅시다. | |
16 April 2023 -- Sewon Park *) | |
Require Import List. |