blob: 0b3a651b3839cce7007fbc5999c0da73573726f9 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
|
module Core.Reduction
import Core.Context
import Core.Declarative
import Core.Term
import Core.Term.Environment
import Core.Term.Substitution
public export
data TermStep : Env sx -> Term sx -> Term sx -> Term sx -> Type where
PiBeta :
TypeWf env f ->
TermWf (env :< f) t g ->
TermWf env u f ->
---
TermStep env (App (Abs n t) u) (subst t $ sub1 u) (subst g $ sub1 u)
AppStep :
TermStep env t u (Pi n f g) ->
TermWf env a f ->
---
TermStep env (App t a) (App u a) (subst g $ sub1 a)
StepConv :
TermStep env t u a ->
TypeConv env a b ->
---
TermStep env t u b
public export
TypeStep : Env sx -> Term sx -> Term sx -> Type
TypeStep env a b = TermStep env a b Set
namespace Type
public export
data TypeRed : Env sx -> Term sx -> Term sx -> Type where
Stay : TypeWf env a -> TypeRed env a a
(::) : TypeStep env a b -> TypeRed env b c -> TypeRed env a c
namespace Term
public export
data TermRed : Env sx -> Term sx -> Term sx -> Term sx -> Type where
Stay : TermWf env t a -> TermRed env t t a
(::) : TermStep env t u a -> TermRed env u v a -> TermRed env t v a
%name TypeStep step
%name TermStep step
%name TypeRed steps
%name TermRed steps
|
