calldecl support and example proof #261

	name: CI
	on: [push, pull_request]
	jobs:
	build-lake:
	runs-on: ubuntu-latest
	steps:
	- name: Checkout current branch (sparse)
	uses: actions/checkout@v4
	with:
	sparse-checkout: \|
	Lampe
	- name: Set up Lean 4
	uses: leanprover/lean-action@v1
	with:
	auto-config: false
	build: false
	test: false
	lint: false
	use-mathlib-cache: true
	lake-package-directory: Lampe
	- name: Build (lake)
	working-directory: Lampe
	run: lake build
	build-cargo:
	runs-on: ubuntu-latest
	steps:
	- name: Checkout current branch
	uses: actions/checkout@v4
	with:
	path: lampe
	- name: "Checkout reilabs/noir (branch: lampe)"
	uses: actions/checkout@v4
	with:
	path: noir
	ref: lampe
	repository: reilabs/noir
	- name: Set up Rust
	uses: actions-rs/toolchain@v1
	with:
	toolchain: stable
	- name: Build (cargo)
	working-directory: lampe
	run: cargo build --release
	test-cargo:
	needs: build-cargo
	runs-on: ubuntu-latest
	steps:
	- name: Checkout current branch
	uses: actions/checkout@v4
	with:
	path: lampe
	- name: "Checkout reilabs/noir (branch: lampe)"
	uses: actions/checkout@v4
	with:
	path: noir
	ref: lampe
	repository: reilabs/noir
	- name: Set up Rust
	uses: actions-rs/toolchain@v1
	with:
	toolchain: stable
	- name: Test (cargo)
	working-directory: lampe
	run: cargo test

Provide feedback