From aaf5034ba2e7fe5811a86121e5c8e2ffc7655e2a Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 13 Aug 2020 14:14:21 -0700 Subject: [PATCH] chore: add helper --- src/Lean/Expr.lean | 15 +++++++++++++++ 1 file changed, 15 insertions(+) diff --git a/src/Lean/Expr.lean b/src/Lean/Expr.lean index 44104ee5f7..4ba294cb21 100644 --- a/src/Lean/Expr.lean +++ b/src/Lean/Expr.lean @@ -202,6 +202,21 @@ instance : Inhabited Expr := | proj _ _ _ d => d | localE _ _ _ d => d +def ctorName : Expr → String +| bvar _ _ => "bvar" +| fvar _ _ => "fvar" +| mvar _ _ => "mvar" +| sort _ _ => "sort" +| const _ _ _ => "const" +| app _ _ _ => "app" +| lam _ _ _ _ => "lam" +| forallE _ _ _ _ => "forallE" +| letE _ _ _ _ _ => "letE" +| lit _ _ => "lit" +| mdata _ _ _ => "mdata" +| proj _ _ _ _ => "proj" +| localE _ _ _ _ => "localE" + def hash (e : Expr) : USize := e.data.hash