lambda_cube_initial_page

|<code haskell> module CubeExpr where

import Char(isAlphaNum, isAlpha) import List(union, (\\)) import Expr import Sub import PreludeExt

freeVars: Expr → [Sym] freeVars (Var s) = [s] freeVars (App f a) = freeVars f union freeVars a freeVars (Lam i t e) = freeVars t union (freeVars e \\ [i]) freeVars (Pi i k t) = freeVars k union (freeVars t \\ [i]) freeVars (Let i t e b) = freeVars (expandLet i t e b) freeVars (Kind _) = emptylist
alphaEq: Expr → Expr → Bool alphaEq (App f a) (App f' a') = alphaEq f f' && alphaEq a a' alphaEq (Lam s t e) (Lam s' t' e') = alphaEq t t' && alphaEq e (substVar s' s e') alphaEq (Pi s k t) (Pi s' k' t') = alphaEq k k' && alphaEq t (substVar s' s t') alphaEq (Let s t e b) (Let s' t' e' b') = alphaEq t t' && alphaEq e e' && alphaEq b (substVar s' s b') alphaEq (Var s) (Var s') = s == s' alphaEq (Kind k) (Kind k') = k == k' alphaEq _ _ = False

</code>|<code haskell> module CliMod where import Expr import CubeExpr

tmp1 x = freeVars x

tmp4 x y = alphaEq x y

</code>|<code haskell> module VarMod where

</code>|<code haskell> module AppMod where

import List(union, (\\))
import Expr

</code> <code haskell> module LamMod where

import List(union, (\\))
import Sub
import Expr

</code> <code haskell> module PiMod where

import List(union, (\\))
import Expr

</code> <code haskell> module LetMod where import Expr

</code> <code haskell> module KindMod where import PreludeExt

</code>

[[internet:view_switcher:examples:lambda_cube|Retour]]