hara.model.annex.spec-lean

!.lean

macro

(!.lean & body)

+book+

+features+

+grammar+

+init+

+meta+

+template+

br

macro

break

macro

catch-all-pattern?

added in 4.1

(catch-all-pattern? pattern)

returns true for broad variable-style fallback patterns

def$.lean

macro

(def$.lean & body)

def.lean

macro

(def.lean & body)

defabstract.lean

macro

(defabstract.lean & body)

defgen.lean

macro

(defgen.lean & body)

defglobal.lean

macro

(defglobal.lean & body)

defmacro.lean

macro

(defmacro.lean & body)

defn-.lean

macro

(defn-.lean & body)

defn.lean

macro

(defn.lean & body)

defptr.lean

macro

(defptr.lean & body)

defrun.lean

macro

(defrun.lean & body)

deftemp.lean

macro

(deftemp.lean & body)

emit-indent-body

added in 4.1

(emit-indent-body [_ form] grammar mopts)

indents the body

emit-raw-str

added in 4.1

(emit-raw-str [_ s] grammar mopts)

emits a raw string

guarded-body

added in 4.1

(guarded-body expr {:keys [guard body]} remaining)

lowers guarded bodies into nested if and fallback match

lean-args

added in 4.1

(lean-args [_ args] grammar mopts)

emit Lean arguments

lean-invoke

added in 4.1

(lean-invoke [sym & args] grammar mopts)

wraps wrappable arguments for function application

match-form

added in 4.1

(match-form expr clauses)

emits a Lean match form

parse-match-clauses

added in 4.1

(parse-match-clauses clauses)

parses shared match clauses

return

macro

set=

macro

tf-defn

added in 4.1

(tf-defn [_ sym args & body])

custom defn for Lean

tf-if

added in 4.1

(tf-if [_ cond then else])

transforms if

tf-lambda

added in 4.1

(tf-lambda [_ args & body])

transforms lambda

tf-letrec

added in 4.1

(tf-letrec [_ bindings & body])

transforms letrec

tf-match

added in 4.1

(tf-match [_ expr & clauses])

transforms match