Commit 57068256 authored by Jean-Christophe Filliâtre's avatar Jean-Christophe Filliâtre
Browse files

theories pour transformations

parent e5f7b46c
theory Prelude
type deco
type undeco
type ty
logic sort(ty,undeco) : deco
end
theory Builtin
use import Prelude
type t
logic tty : ty
logic d2t(deco) : t
logic t2u(t) : undeco
axiom Conv : forall x:t[t2u(x)]. d2t(sort(tty,t2u(x)))=x
end
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment