Commit 2790390f authored by marton bognar's avatar marton bognar
Browse files

Add specification for STLC Prod

parent 081b108f
namespace TermVar: Term
sort Term
inh ctx TermVar
| Var (x@ctx)
| Lam (t: Term) [x: TermVar]
t.ctx = lhs.ctx, x
| App (t1: Term) (t2: Term)
| Prod (t1: Term) (t2: Term)
| Let (p: Pat) (t1: Term) (t2: Term)
p.ictx = lhs.ctx
t2.ctx = p.sctx
sort Pat
inh ictx TermVar
syn sctx TermVar
| PVar (x: TermVar)
lhs.sctx = lhs.ictx, x
| PProd (p1: Pat) (p2: Pat)
p1.ictx = lhs.ictx
p2.ictx = p1.sctx
lhs.sctx = p2.sctx
Supports Markdown
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