mirror of
https://github.com/c-cube/sidekick.git
synced 2025-12-06 03:05:31 -05:00
25 lines
881 B
Text
25 lines
881 B
Text
t1: f (g x) y
|
|
loc(t1): 1 | f (g x) y
|
|
^^^^^^^^^
|
|
|
|
t2: let x := 1 in f (f x 2)
|
|
loc(t2): 1 | let x:= 1 in f (f x 2)
|
|
^^^^^^^^^^^^^^^^^^^^^^
|
|
|
|
t3: let l := map f (list 1 2 3) in let l2 := rev l in = (rev l2) l
|
|
loc(t3): 1 | let l := map f (list 1 2 3) in
|
|
1 | let l2 := rev l in rev l2 = l
|
|
|
|
t4: let assm := ==> (is_foo p) (= (filter p l) nil) in true
|
|
loc(t4): 1 | let assm := is_foo p ==> (filter p l = nil) in true
|
|
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
|
|
|
|
t5: let f := lam (x y : int) (z : bool). (= (+ x y) z)
|
|
and g := lam x. (f (f x)) in is_g g
|
|
loc(t5): 1 | let f := fn (x y : int) (z:bool). ( x+ y) = z
|
|
1 | and g := fn x. f (f x) in is_g g
|
|
|
|
d1:
|
|
def f (x y : list int) : list int := if (= x 0) y whatever;
|
|
#ty f;
|
|
#sledgehammer lam x y. (= (f x y) (f x y));
|