Advertisement
Not a member of Pastebin yet?
Sign Up,
it unlocks many cool features!
- Require Import Coq.Lists.List.
- Set Implicit Arguments.
- Inductive type : Set :=
- | TNat : type
- | TArrow : type -> type -> type.
- Definition ctx := list type.
- Inductive var : ctx -> type -> Set :=
- | VarZ : forall t Gamma, var (t :: Gamma) t
- | VarS : forall s t Gamma, var Gamma t -> var (s :: Gamma) t.
- Inductive tm (Gamma : ctx) : type -> Set :=
- | Lit : nat -> tm Gamma TNat
- | Add : tm Gamma TNat -> tm Gamma TNat -> tm Gamma TNat
- | Var : forall t, var Gamma t -> tm Gamma t
- | Lam : forall s t, tm (s :: Gamma) t -> tm Gamma (TArrow s t)
- | App : forall s t, tm Gamma (TArrow s t) -> tm Gamma s -> tm Gamma t.
- Class Bridge (A : Type) :=
- { ty : type ;
- reflect : forall {Gamma}, A -> tm Gamma ty ;
- reify : forall {Gamma}, tm Gamma ty -> option A ;
- }.
- Instance nat_Bridge : Bridge nat :=
- { ty := TNat ;
- reflect {Gamma} n := Lit Gamma n ;
- reify {Gamma} e :=
- match e with
- | Lit _ n => Some n
- | _ => None
- end ;
- }.
Advertisement
Add Comment
Please, Sign In to add comment
Advertisement