Dimitur Krustev dkrustev
dkrustev
/ Unify.agda
Created
April 20, 2016 12:28
— forked from copumpkin/Unify.agda
Structurally recursive unification à la McBride
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
| module Unify where | |
| -- Translated from http://strictlypositive.org/unify.ps.gz | |
| open import Data.Empty | |
| import Data.Maybe as Maybe | |
| open Maybe hiding (map) | |
| open import Data.Nat | |
| open import Data.Fin | |
| open import Data.Product hiding (map) |
dkrustev
/ EasyTypeSafety.v
Created
June 29, 2013 07:59
Coq formalization of http://siek.blogspot.com/2013/05/type-safety-in-three-easy-lemmas.html
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
| (* author: Dimitur Krustev *) | |
| (* started: 20130616 *) | |
| (* based on: http://siek.blogspot.com/2013/05/type-safety-in-three-easy-lemmas.html *) | |
| Require Import Arith List Bool. | |
| Set Implicit Arguments. | |
| Section Lang. |