Commit 08702e51 authored by Raphaël Cauderlier's avatar Raphaël Cauderlier
Browse files

Use "let" instead of "var" to introduce terms

parent a7dd359b
......@@ -22,7 +22,7 @@ rule token = parse
| "->" { ARR }
| "λ" { LAMBDA }
| "type" { TYPE (Parsing.rhs_start_pos 1) }
| "var" { VAR (Parsing.rhs_start_pos 1) }
| "let" { VAR (Parsing.rhs_start_pos 1) }
| "check" { CHECK (Parsing.rhs_start_pos 1) }
| "norm" { NORM (Parsing.rhs_start_pos 1) }
| [ 'a'-'z' ] ['a'-'z' 'A'-'Z' '_' '0'-'9']* as s { ID (s) }
......
......@@ -3,18 +3,20 @@ type A ::= [ a : [] ].
type Bool ::= [ if : A ; then : A ; else : A ].
var true : Bool ::= [ if = ς(x : Bool) x.then ;
type Arrow ::= [ arg : A ; val : A ].
let true : Bool ::= [ if = ς(x : Bool) x.then ;
then = ς(x : Bool) x.then ;
else = ς(x : Bool) x.else ].
var false : Bool ::= [ if = ς(x : Bool) x.else ;
let false : Bool ::= [ if = ς(x : Bool) x.else ;
then = ς(x : Bool) x.then ;
else = ς(x : Bool) x.else ].
var if : Bool -> A -> A -> A ::=
let if : Bool -> A -> A -> A ::=
λ(b : Bool) λ(t : A) λ(e : A) ((b.then := t).else := e).if.
type Nat ::= [ iszero : Bool ;
pred : A ].
var 0 : Nat ::= [ iszero = ς(x : Nat) true ;
let 0 : Nat ::= [ iszero = ς(x : Nat) true ;
pred = ς(x : Nat) x.pred ].
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