max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

test(tests/playground/inst): add instantiate and instantiateRev simple tests

Browse source
This commit is contained in:
Leonardo de Moura 2019-09-16 18:30:35 -07:00
parent 704f90d728
commit 6d7041fcb4
1 changed files with 16 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

16
tests/playground/inst.lean Normal file
View file

@ -0,0 +1,16 @@
import init.lean.expr
open Lean
def main (xs : List String) : IO Unit :=
do
let f := mkConst `f;
let x := Expr.bvar 0;
let y := Expr.bvar 1;
let t := Expr.app (Expr.app (Expr.app f x) y) x;
let a := mkConst `a;
let b := Expr.app f (mkConst `b);
IO.println t.dbgToString;
IO.println (t.instantiate [a, b].toArray).dbgToString;
IO.println (t.instantiateRev [a, b].toArray).dbgToString;
IO.println (t.instantiate [a].toArray).dbgToString;
pure ()