Computation and Deduction 2009/20090304-support
From The Twelf Project
| This is Literate Twelf Code: here Status: %% ABORT %% Output: here. |
Support code for March 4 guest lecture on worlds-checking and combinators.
% combinator equality
ceq : comb -> comb -> type.
% betas
ceq/i : ceq (capp i A) A.
ceq/k : ceq (capp (capp k A) B) A.
ceq/s : ceq (capp (capp (capp s A) B) C) (capp (capp A C) (capp B C)).
% extensionality
ceq/ext : ceq A A'
<- ({y:comb} ceq (capp A y) (capp A' y)).
% compatibility
ceq/app : ceq (capp A B) (capp A' B')
<- ceq A A'
<- ceq B B'.
% equivalence
ceq/refl : ceq A A.
ceq/symm : ceq A A'
<- ceq A' A.
ceq/trans : ceq A A'
<- ceq A B
<- ceq B A'.
%worlds (comb-block) (ceq _ _).
