Skip to content

Instantly share code, notes, and snippets.

View park-sewon's full-sized avatar
🎇

Sewon Park park-sewon

🎇
View GitHub Profile
@park-sewon
park-sewon / practice_coq_1.v
Created April 16, 2023 09:32
A simple Coq practice session
(* Context와 state가 있는 프로그래밍 언어를 정형화하고자 합니다.
프로그래밍 변수로는 De Brujin index를 사용할 것이며,
따라서 context는 단순히 데이터 타입들의 리스트 입니다.
(예를 들어서 int :: int :: boolean :: nil 이 하나의 context입니다.
리스트를 사용해서 생기는 문제를 해결해 봅시다.
16 April 2023 -- Sewon Park *)
Require Import List.