diff options
| author | aarne <unknown> | 2004-09-19 20:27:38 +0000 |
|---|---|---|
| committer | aarne <unknown> | 2004-09-19 20:27:38 +0000 |
| commit | 0e21dcbf543f9a0367e69abd7f5f19b7852911e3 (patch) | |
| tree | 17f439f9732ea405f1325b81d51c65d8ec37b433 /grammars | |
| parent | df4cbb482f0546b884eb210d825c794d14f82712 (diff) | |
Imper
Diffstat (limited to 'grammars')
| -rw-r--r-- | grammars/prelude/Prelude.gf | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/grammars/prelude/Prelude.gf b/grammars/prelude/Prelude.gf index 385a734ec..d124d7df6 100644 --- a/grammars/prelude/Prelude.gf +++ b/grammars/prelude/Prelude.gf @@ -29,6 +29,8 @@ oper postfixSS : Str -> SS -> SS = \f,x -> ss (x.s ++ f) ; embedSS : Str -> Str -> SS -> SS = \f,g,x -> ss (f ++ x.s ++ g) ; + id : (A : Type) -> A -> A ; + -- discontinuous SD2 = {s1,s2 : Str} ; sd2 : (_,_ : Str) -> SD2 = \x,y -> {s1 = x ; s2 = y} ; |