30 lines
561 B
Text
30 lines
561 B
Text
|
|
[init]
|
|
def sefFn (x_1 : obj) (x_2 : obj) : obj :=
|
|
case x_1 : obj of
|
|
Lean.Expr.bvar →
|
|
ret x_1
|
|
Lean.Expr.fvar →
|
|
ret x_1
|
|
Lean.Expr.mvar →
|
|
ret x_1
|
|
Lean.Expr.sort →
|
|
ret x_1
|
|
Lean.Expr.const →
|
|
ret x_1
|
|
Lean.Expr.app →
|
|
let x_3 : obj := proj[1] x_1;
|
|
let x_4 : obj := Lean.Expr.updateApp x_1 x_2 x_3 ◾;
|
|
ret x_4
|
|
Lean.Expr.lam →
|
|
ret x_1
|
|
Lean.Expr.forallE →
|
|
ret x_1
|
|
Lean.Expr.letE →
|
|
ret x_1
|
|
Lean.Expr.lit →
|
|
ret x_1
|
|
Lean.Expr.mdata →
|
|
ret x_1
|
|
Lean.Expr.proj →
|
|
ret x_1
|